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 ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( chr ‘ ( 𝑅 ↾s 𝐴 ) ) = ( chr ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 subrgsubg ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ ( SubGrp ‘ 𝑅 ) )
2 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
3 2 subrg1cl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝐴 )
4 eqid ⊢ ( 𝑅 ↾s 𝐴 ) = ( 𝑅 ↾s 𝐴 )
5 eqid ⊢ ( od ‘ 𝑅 ) = ( od ‘ 𝑅 )
6 eqid ⊢ ( od ‘ ( 𝑅 ↾s 𝐴 ) ) = ( od ‘ ( 𝑅 ↾s 𝐴 ) )
7 4 5 6 subgod ⊢ ( ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) → ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( od ‘ ( 𝑅 ↾s 𝐴 ) ) ‘ ( 1r ‘ 𝑅 ) ) )
8 1 3 7 syl2anc ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( od ‘ ( 𝑅 ↾s 𝐴 ) ) ‘ ( 1r ‘ 𝑅 ) ) )
9 4 2 subrg1 ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( 𝑅 ↾s 𝐴 ) ) )
10 9 fveq2d ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ( od ‘ ( 𝑅 ↾s 𝐴 ) ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( od ‘ ( 𝑅 ↾s 𝐴 ) ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝐴 ) ) ) )
11 8 10 eqtr2d ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ( od ‘ ( 𝑅 ↾s 𝐴 ) ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝐴 ) ) ) = ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
12 eqid ⊢ ( 1r ‘ ( 𝑅 ↾s 𝐴 ) ) = ( 1r ‘ ( 𝑅 ↾s 𝐴 ) )
13 eqid ⊢ ( chr ‘ ( 𝑅 ↾s 𝐴 ) ) = ( chr ‘ ( 𝑅 ↾s 𝐴 ) )
14 6 12 13 chrval ⊢ ( ( od ‘ ( 𝑅 ↾s 𝐴 ) ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝐴 ) ) ) = ( chr ‘ ( 𝑅 ↾s 𝐴 ) )
15 eqid ⊢ ( chr ‘ 𝑅 ) = ( chr ‘ 𝑅 )
16 5 2 15 chrval ⊢ ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = ( chr ‘ 𝑅 )
17 11 14 16 3eqtr3g ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( chr ‘ ( 𝑅 ↾s 𝐴 ) ) = ( chr ‘ 𝑅 ) )