gsummgp0

Description: If one factor in a finite group sum of the multiplicative group of a commutative ring is 0, the whole "sum" (i.e. product) is 0. (Contributed by AV, 3-Jan-2019)

	Ref	Expression
Hypotheses	gsummgp0.g	$⊢ G = {mulGrp}_{R}$
	gsummgp0.0	$⊢ \underset{˙}{0} = 0_{R}$
	gsummgp0.r	$⊢ φ \to R \in CRing$
	gsummgp0.n	$⊢ φ \to N \in Fin$
	gsummgp0.a	$⊢ (φ \land n \in N) \to A \in {Base}_{R}$
	gsummgp0.e	$⊢ (φ \land n = i) \to A = B$
	gsummgp0.b	$⊢ φ \to \exists i \in N B = \underset{˙}{0}$
Assertion	gsummgp0	$⊢ φ \to \underset{n \in N}{\sum_{G}} A = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		gsummgp0.g	$⊢ G = {mulGrp}_{R}$
2		gsummgp0.0	$⊢ \underset{˙}{0} = 0_{R}$
3		gsummgp0.r	$⊢ φ \to R \in CRing$
4		gsummgp0.n	$⊢ φ \to N \in Fin$
5		gsummgp0.a	$⊢ (φ \land n \in N) \to A \in {Base}_{R}$
6		gsummgp0.e	$⊢ (φ \land n = i) \to A = B$
7		gsummgp0.b	$⊢ φ \to \exists i \in N B = \underset{˙}{0}$
8		difsnid	$⊢ i \in N \to (N ∖ \{i\}) \cup \{i\} = N$
9	8	eqcomd	$⊢ i \in N \to N = (N ∖ \{i\}) \cup \{i\}$
10	9	ad2antrl	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to N = (N ∖ \{i\}) \cup \{i\}$
11	10	mpteq1d	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to (n \in N ⟼ A) = (n \in ((N ∖ \{i\}) \cup \{i\}) ⟼ A)$
12	11	oveq2d	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to \underset{n \in N}{\sum_{G}} A = \underset{n \in (N ∖ \{i\}) \cup \{i\}}{\sum_{G}} A$
13		eqid	$⊢ {Base}_{R} = {Base}_{R}$
14	1 13	mgpbas	$⊢ {Base}_{R} = {Base}_{G}$
15		eqid	$⊢ \cdot_{R} = \cdot_{R}$
16	1 15	mgpplusg	$⊢ \cdot_{R} = +_{G}$
17	1	crngmgp	$⊢ R \in CRing \to G \in CMnd$
18	3 17	syl	$⊢ φ \to G \in CMnd$
19	18	adantr	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to G \in CMnd$
20		diffi	$⊢ N \in Fin \to N ∖ \{i\} \in Fin$
21	4 20	syl	$⊢ φ \to N ∖ \{i\} \in Fin$
22	21	adantr	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to N ∖ \{i\} \in Fin$
23		simpl	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to φ$
24		eldifi	$⊢ n \in (N ∖ \{i\}) \to n \in N$
25	23 24 5	syl2an	$⊢ ((φ \land (i \in N \land B = \underset{˙}{0})) \land n \in (N ∖ \{i\})) \to A \in {Base}_{R}$
26		simprl	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to i \in N$
27		neldifsnd	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to \neg i \in (N ∖ \{i\})$
28		crngring	$⊢ R \in CRing \to R \in Ring$
29	3 28	syl	$⊢ φ \to R \in Ring$
30		ringmnd	$⊢ R \in Ring \to R \in Mnd$
31	13 2	mndidcl	$⊢ R \in Mnd \to \underset{˙}{0} \in {Base}_{R}$
32	29 30 31	3syl	$⊢ φ \to \underset{˙}{0} \in {Base}_{R}$
33	32	adantr	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to \underset{˙}{0} \in {Base}_{R}$
34		eleq1	$⊢ B = \underset{˙}{0} \to (B \in {Base}_{R} \leftrightarrow \underset{˙}{0} \in {Base}_{R})$
35	34	ad2antll	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to (B \in {Base}_{R} \leftrightarrow \underset{˙}{0} \in {Base}_{R})$
36	33 35	mpbird	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to B \in {Base}_{R}$
37	6	adantlr	$⊢ ((φ \land (i \in N \land B = \underset{˙}{0})) \land n = i) \to A = B$
38	14 16 19 22 25 26 27 36 37	gsumunsnd	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to \underset{n \in (N ∖ \{i\}) \cup \{i\}}{\sum_{G}} A = (\underset{n \in N ∖ \{i\}}{\sum_{G}}, A) \cdot_{R} B$
39		oveq2	$⊢ B = \underset{˙}{0} \to (\underset{n \in N ∖ \{i\}}{\sum_{G}}, A) \cdot_{R} B = (\underset{n \in N ∖ \{i\}}{\sum_{G}}, A) \cdot_{R} \underset{˙}{0}$
40	39	ad2antll	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to (\underset{n \in N ∖ \{i\}}{\sum_{G}}, A) \cdot_{R} B = (\underset{n \in N ∖ \{i\}}{\sum_{G}}, A) \cdot_{R} \underset{˙}{0}$
41	24 5	sylan2	$⊢ (φ \land n \in (N ∖ \{i\})) \to A \in {Base}_{R}$
42	41	ralrimiva	$⊢ φ \to \forall n \in (N ∖ \{i\}) A \in {Base}_{R}$
43	14 18 21 42	gsummptcl	$⊢ φ \to \underset{n \in N ∖ \{i\}}{\sum_{G}} A \in {Base}_{R}$
44	43	adantr	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to \underset{n \in N ∖ \{i\}}{\sum_{G}} A \in {Base}_{R}$
45	13 15 2	ringrz	$⊢ (R \in Ring \land \underset{n \in N ∖ \{i\}}{\sum_{G}} A \in {Base}_{R}) \to (\underset{n \in N ∖ \{i\}}{\sum_{G}}, A) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
46	29 44 45	syl2an2r	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to (\underset{n \in N ∖ \{i\}}{\sum_{G}}, A) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
47	40 46	eqtrd	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to (\underset{n \in N ∖ \{i\}}{\sum_{G}}, A) \cdot_{R} B = \underset{˙}{0}$
48	12 38 47	3eqtrd	$⊢ (φ \land (i \in N \land B = \underset{˙}{0})) \to \underset{n \in N}{\sum_{G}} A = \underset{˙}{0}$
49	7 48	rexlimddv	$⊢ φ \to \underset{n \in N}{\sum_{G}} A = \underset{˙}{0}$

Metamath Proof Explorer

Theorem gsummgp0

Proof