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 ‘ 𝑅 ) )