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 \in SubRing (R) \to chr (R ↾_{𝑠} A) = chr (R)$

Step	Hyp	Ref	Expression
1		subrgsubg	$⊢ A \in SubRing (R) \to A \in SubGrp (R)$
2		eqid	$⊢ 1_{R} = 1_{R}$
3	2	subrg1cl	$⊢ A \in SubRing (R) \to 1_{R} \in 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 \in SubGrp (R) \land 1_{R} \in A) \to od (R) (1_{R}) = od (R ↾_{𝑠} A) (1_{R})$
8	1 3 7	syl2anc	$⊢ A \in SubRing (R) \to od (R) (1_{R}) = od (R ↾_{𝑠} A) (1_{R})$
9	4 2	subrg1	$⊢ A \in SubRing (R) \to 1_{R} = 1_{(R ↾_{𝑠} A)}$
10	9	fveq2d	$⊢ A \in SubRing (R) \to od (R ↾_{𝑠} A) (1_{R}) = od (R ↾_{𝑠} A) (1_{(R ↾_{𝑠} A)})$
11	8 10	eqtr2d	$⊢ A \in SubRing (R) \to 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 \in SubRing (R) \to chr (R ↾_{𝑠} A) = chr (R)$

Metamath Proof Explorer