This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subrgchr

Description: If A is a subring of R , then they have the same characteristic. (Contributed by Thierry Arnoux, 24-Feb-2018)

Ref Expression
Assertion subrgchr ⊢ A ∈ SubRing ⁡ R → chr ⁡ R ↾ 𝑠 A = chr ⁡ R

Proof

Step Hyp Ref Expression
1 subrgsubg ⊢ A ∈ SubRing ⁡ R → A ∈ SubGrp ⁡ R
2 eqid ⊢ 1 R = 1 R
3 2 subrg1cl ⊢ A ∈ SubRing ⁡ R → 1 R ∈ A
4 eqid ⊢ R ↾ 𝑠 A = R ↾ 𝑠 A
5 eqid ⊢ od ⁡ R = od ⁡ R
6 eqid ⊢ od ⁡ R ↾ 𝑠 A = od ⁡ R ↾ 𝑠 A
7 4 5 6 subgod ⊢ A ∈ SubGrp ⁡ R ∧ 1 R ∈ A → od ⁡ R ⁡ 1 R = od ⁡ R ↾ 𝑠 A ⁡ 1 R
8 1 3 7 syl2anc ⊢ A ∈ SubRing ⁡ R → od ⁡ R ⁡ 1 R = od ⁡ R ↾ 𝑠 A ⁡ 1 R
9 4 2 subrg1 ⊢ A ∈ SubRing ⁡ R → 1 R = 1 R ↾ 𝑠 A
10 9 fveq2d ⊢ A ∈ SubRing ⁡ R → od ⁡ R ↾ 𝑠 A ⁡ 1 R = od ⁡ R ↾ 𝑠 A ⁡ 1 R ↾ 𝑠 A
11 8 10 eqtr2d ⊢ A ∈ SubRing ⁡ R → od ⁡ R ↾ 𝑠 A ⁡ 1 R ↾ 𝑠 A = od ⁡ R ⁡ 1 R
12 eqid ⊢ 1 R ↾ 𝑠 A = 1 R ↾ 𝑠 A
13 eqid ⊢ chr ⁡ R ↾ 𝑠 A = chr ⁡ R ↾ 𝑠 A
14 6 12 13 chrval ⊢ od ⁡ R ↾ 𝑠 A ⁡ 1 R ↾ 𝑠 A = chr ⁡ R ↾ 𝑠 A
15 eqid ⊢ chr ⁡ R = chr ⁡ R
16 5 2 15 chrval ⊢ od ⁡ R ⁡ 1 R = chr ⁡ R
17 11 14 16 3eqtr3g ⊢ A ∈ SubRing ⁡ R → chr ⁡ R ↾ 𝑠 A = chr ⁡ R