dvdschrmulg

Description: In a ring, any multiple of the characteristics annihilates all elements. (Contributed by Thierry Arnoux, 6-Sep-2016)

	Ref	Expression
Hypotheses	dvdschrmulg.1	$⊢ C = chr (R)$
	dvdschrmulg.2	$⊢ B = {Base}_{R}$
	dvdschrmulg.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	dvdschrmulg.4	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	dvdschrmulg	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to N \underset{˙}{\cdot} A = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		dvdschrmulg.1	$⊢ C = chr (R)$
2		dvdschrmulg.2	$⊢ B = {Base}_{R}$
3		dvdschrmulg.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		dvdschrmulg.4	$⊢ \underset{˙}{0} = 0_{R}$
5		simp1	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to R \in Ring$
6		dvdszrcl	$⊢ C ∥ N \to (C \in ℤ \land N \in ℤ)$
7	6	simprd	$⊢ C ∥ N \to N \in ℤ$
8	7	3ad2ant2	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to N \in ℤ$
9		eqid	$⊢ 1_{R} = 1_{R}$
10	2 9	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
11	5 10	syl	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to 1_{R} \in B$
12		simp3	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to A \in B$
13		eqid	$⊢ \cdot_{R} = \cdot_{R}$
14	2 3 13	mulgass2	$⊢ (R \in Ring \land (N \in ℤ \land 1_{R} \in B \land A \in B)) \to (N \underset{˙}{\cdot} 1_{R}) \cdot_{R} A = N \underset{˙}{\cdot} (1_{R} \cdot_{R} A)$
15	5 8 11 12 14	syl13anc	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to (N \underset{˙}{\cdot} 1_{R}) \cdot_{R} A = N \underset{˙}{\cdot} (1_{R} \cdot_{R} A)$
16		ringgrp	$⊢ R \in Ring \to R \in Grp$
17	5 16	syl	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to R \in Grp$
18		eqid	$⊢ od (R) = od (R)$
19	18 9 1	chrval	$⊢ od (R) (1_{R}) = C$
20		simp2	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to C ∥ N$
21	19 20	eqbrtrid	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to od (R) (1_{R}) ∥ N$
22	2 18 3 4	oddvdsi	$⊢ (R \in Grp \land 1_{R} \in B \land od (R) (1_{R}) ∥ N) \to N \underset{˙}{\cdot} 1_{R} = \underset{˙}{0}$
23	17 11 21 22	syl3anc	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to N \underset{˙}{\cdot} 1_{R} = \underset{˙}{0}$
24	23	oveq1d	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to (N \underset{˙}{\cdot} 1_{R}) \cdot_{R} A = \underset{˙}{0} \cdot_{R} A$
25	2 13 4	ringlz	$⊢ (R \in Ring \land A \in B) \to \underset{˙}{0} \cdot_{R} A = \underset{˙}{0}$
26	25	3adant2	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to \underset{˙}{0} \cdot_{R} A = \underset{˙}{0}$
27	24 26	eqtrd	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to (N \underset{˙}{\cdot} 1_{R}) \cdot_{R} A = \underset{˙}{0}$
28	2 13 9	ringlidm	$⊢ (R \in Ring \land A \in B) \to 1_{R} \cdot_{R} A = A$
29	28	3adant2	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to 1_{R} \cdot_{R} A = A$
30	29	oveq2d	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to N \underset{˙}{\cdot} (1_{R} \cdot_{R} A) = N \underset{˙}{\cdot} A$
31	15 27 30	3eqtr3rd	$⊢ (R \in Ring \land C ∥ N \land A \in B) \to N \underset{˙}{\cdot} A = \underset{˙}{0}$

Metamath Proof Explorer

Theorem dvdschrmulg

Proof