idomnnzgmulnz

Description: A finite product of nonzero elements in an integral domain is nonzero. (Contributed by metakunt, 5-May-2025)

	Ref	Expression
Hypotheses	idomnnzgmulnz.1	$⊢ G = {mulGrp}_{R}$
	idomnnzgmulnz.2	$⊢ φ \to R \in IDomn$
	idomnnzgmulnz.3	$⊢ φ \to N \in Fin$
	idomnnzgmulnz.4	$⊢ (φ \land n \in N) \to A \in {Base}_{R}$
	idomnnzgmulnz.5	$⊢ (φ \land n \in N) \to A \neq 0_{R}$
Assertion	idomnnzgmulnz	$⊢ φ \to \underset{n \in N}{\sum_{G}} A \neq 0_{R}$

Proof

Step	Hyp	Ref	Expression
1		idomnnzgmulnz.1	$⊢ G = {mulGrp}_{R}$
2		idomnnzgmulnz.2	$⊢ φ \to R \in IDomn$
3		idomnnzgmulnz.3	$⊢ φ \to N \in Fin$
4		idomnnzgmulnz.4	$⊢ (φ \land n \in N) \to A \in {Base}_{R}$
5		idomnnzgmulnz.5	$⊢ (φ \land n \in N) \to A \neq 0_{R}$
6		mpteq1	$⊢ x = \emptyset \to (n \in x ⟼ A) = (n \in \emptyset ⟼ A)$
7	6	oveq2d	$⊢ x = \emptyset \to \underset{n \in x}{\sum_{G}} A = \underset{n \in \emptyset}{\sum_{G}} A$
8	7	neeq1d	$⊢ x = \emptyset \to (\underset{n \in x}{\sum_{G}} A \neq 0_{R} \leftrightarrow \underset{n \in \emptyset}{\sum_{G}} A \neq 0_{R})$
9		mpteq1	$⊢ x = y \to (n \in x ⟼ A) = (n \in y ⟼ A)$
10	9	oveq2d	$⊢ x = y \to \underset{n \in x}{\sum_{G}} A = \underset{n \in y}{\sum_{G}} A$
11	10	neeq1d	$⊢ x = y \to (\underset{n \in x}{\sum_{G}} A \neq 0_{R} \leftrightarrow \underset{n \in y}{\sum_{G}} A \neq 0_{R})$
12		mpteq1	$⊢ x = y \cup \{z\} \to (n \in x ⟼ A) = (n \in (y \cup \{z\}) ⟼ A)$
13	12	oveq2d	$⊢ x = y \cup \{z\} \to \underset{n \in x}{\sum_{G}} A = \underset{n \in y \cup \{z\}}{\sum_{G}} A$
14	13	neeq1d	$⊢ x = y \cup \{z\} \to (\underset{n \in x}{\sum_{G}} A \neq 0_{R} \leftrightarrow \underset{n \in y \cup \{z\}}{\sum_{G}} A \neq 0_{R})$
15		mpteq1	$⊢ x = N \to (n \in x ⟼ A) = (n \in N ⟼ A)$
16	15	oveq2d	$⊢ x = N \to \underset{n \in x}{\sum_{G}} A = \underset{n \in N}{\sum_{G}} A$
17	16	neeq1d	$⊢ x = N \to (\underset{n \in x}{\sum_{G}} A \neq 0_{R} \leftrightarrow \underset{n \in N}{\sum_{G}} A \neq 0_{R})$
18		mpt0	$⊢ (n \in \emptyset ⟼ A) = \emptyset$
19	18	a1i	$⊢ φ \to (n \in \emptyset ⟼ A) = \emptyset$
20	19	oveq2d	$⊢ φ \to \underset{n \in \emptyset}{\sum_{G}} A = \sum_{G} \emptyset$
21		eqid	$⊢ 0_{G} = 0_{G}$
22	21	gsum0	$⊢ \sum_{G} \emptyset = 0_{G}$
23	22	a1i	$⊢ φ \to \sum_{G} \emptyset = 0_{G}$
24	20 23	eqtrd	$⊢ φ \to \underset{n \in \emptyset}{\sum_{G}} A = 0_{G}$
25		eqid	$⊢ 1_{R} = 1_{R}$
26	1 25	ringidval	$⊢ 1_{R} = 0_{G}$
27	26	eqcomi	$⊢ 0_{G} = 1_{R}$
28	27	a1i	$⊢ φ \to 0_{G} = 1_{R}$
29		isidom	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in Domn)$
30	29	simprbi	$⊢ R \in IDomn \to R \in Domn$
31		domnnzr	$⊢ R \in Domn \to R \in NzRing$
32		eqid	$⊢ 0_{R} = 0_{R}$
33	25 32	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
34	2 30 31 33	4syl	$⊢ φ \to 1_{R} \neq 0_{R}$
35	28 34	eqnetrd	$⊢ φ \to 0_{G} \neq 0_{R}$
36	24 35	eqnetrd	$⊢ φ \to \underset{n \in \emptyset}{\sum_{G}} A \neq 0_{R}$
37		nfcv	$⊢ \underline{Ⅎ} m A$
38		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ m / n ⦌ A$
39		csbeq1a	$⊢ n = m \to A = ⦋ m / n ⦌ A$
40	37 38 39	cbvmpt	$⊢ (n \in (y \cup \{z\}) ⟼ A) = (m \in (y \cup \{z\}) ⟼ ⦋ m / n ⦌ A)$
41	40	oveq2i	$⊢ \underset{n \in y \cup \{z\}}{\sum_{G}} A = \underset{m \in y \cup \{z\}}{\sum_{G}} ⦋ m / n ⦌ A$
42	41	a1i	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to \underset{n \in y \cup \{z\}}{\sum_{G}} A = \underset{m \in y \cup \{z\}}{\sum_{G}} ⦋ m / n ⦌ A$
43		eqid	$⊢ {Base}_{G} = {Base}_{G}$
44		eqid	$⊢ +_{G} = +_{G}$
45	29	simplbi	$⊢ R \in IDomn \to R \in CRing$
46	2 45	syl	$⊢ φ \to R \in CRing$
47	1	crngmgp	$⊢ R \in CRing \to G \in CMnd$
48	46 47	syl	$⊢ φ \to G \in CMnd$
49	48	adantr	$⊢ (φ \land (y \subseteq N \land z \in (N ∖ y))) \to G \in CMnd$
50	49	adantr	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to G \in CMnd$
51	3	adantr	$⊢ (φ \land (y \subseteq N \land z \in (N ∖ y))) \to N \in Fin$
52		simprl	$⊢ (φ \land (y \subseteq N \land z \in (N ∖ y))) \to y \subseteq N$
53	51 52	ssfid	$⊢ (φ \land (y \subseteq N \land z \in (N ∖ y))) \to y \in Fin$
54	53	adantr	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to y \in Fin$
55	52	ad2antrr	$⊢ (((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \land m \in y) \to y \subseteq N$
56		simpr	$⊢ (((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \land m \in y) \to m \in y$
57	55 56	sseldd	$⊢ (((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \land m \in y) \to m \in N$
58	4	ralrimiva	$⊢ φ \to \forall n \in N A \in {Base}_{R}$
59	58	ad3antrrr	$⊢ (((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \land m \in y) \to \forall n \in N A \in {Base}_{R}$
60		rspcsbela	$⊢ (m \in N \land \forall n \in N A \in {Base}_{R}) \to ⦋ m / n ⦌ A \in {Base}_{R}$
61	57 59 60	syl2anc	$⊢ (((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \land m \in y) \to ⦋ m / n ⦌ A \in {Base}_{R}$
62		eqid	$⊢ {Base}_{R} = {Base}_{R}$
63	1 62	mgpbas	$⊢ {Base}_{R} = {Base}_{G}$
64	63	a1i	$⊢ (((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \land m \in y) \to {Base}_{R} = {Base}_{G}$
65	61 64	eleqtrd	$⊢ (((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \land m \in y) \to ⦋ m / n ⦌ A \in {Base}_{G}$
66		eldifi	$⊢ z \in (N ∖ y) \to z \in N$
67	66	adantl	$⊢ (y \subseteq N \land z \in (N ∖ y)) \to z \in N$
68	67	adantl	$⊢ (φ \land (y \subseteq N \land z \in (N ∖ y))) \to z \in N$
69	68	adantr	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to z \in N$
70		eldifn	$⊢ z \in (N ∖ y) \to \neg z \in y$
71	70	adantl	$⊢ (y \subseteq N \land z \in (N ∖ y)) \to \neg z \in y$
72	71	adantl	$⊢ (φ \land (y \subseteq N \land z \in (N ∖ y))) \to \neg z \in y$
73	72	adantr	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to \neg z \in y$
74	58	ad2antrr	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to \forall n \in N A \in {Base}_{R}$
75		rspcsbela	$⊢ (z \in N \land \forall n \in N A \in {Base}_{R}) \to ⦋ z / n ⦌ A \in {Base}_{R}$
76	69 74 75	syl2anc	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to ⦋ z / n ⦌ A \in {Base}_{R}$
77	63	a1i	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to {Base}_{R} = {Base}_{G}$
78	76 77	eleqtrd	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to ⦋ z / n ⦌ A \in {Base}_{G}$
79		csbeq1	$⊢ m = z \to ⦋ m / n ⦌ A = ⦋ z / n ⦌ A$
80	43 44 50 54 65 69 73 78 79	gsumunsn	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to \underset{m \in y \cup \{z\}}{\sum_{G}} ⦋ m / n ⦌ A = (\underset{m \in y}{\sum_{G}}, ⦋ m / n ⦌ A) +_{G} ⦋ z / n ⦌ A$
81	42 80	eqtrd	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to \underset{n \in y \cup \{z\}}{\sum_{G}} A = (\underset{m \in y}{\sum_{G}}, ⦋ m / n ⦌ A) +_{G} ⦋ z / n ⦌ A$
82	2 30	syl	$⊢ φ \to R \in Domn$
83	82	adantr	$⊢ (φ \land (y \subseteq N \land z \in (N ∖ y))) \to R \in Domn$
84	83	adantr	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to R \in Domn$
85	61	ralrimiva	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to \forall m \in y ⦋ m / n ⦌ A \in {Base}_{R}$
86	63 50 54 85	gsummptcl	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to \underset{m \in y}{\sum_{G}} ⦋ m / n ⦌ A \in {Base}_{R}$
87	39	equcoms	$⊢ m = n \to A = ⦋ m / n ⦌ A$
88	87	eqcomd	$⊢ m = n \to ⦋ m / n ⦌ A = A$
89	38 37 88	cbvmpt	$⊢ (m \in y ⟼ ⦋ m / n ⦌ A) = (n \in y ⟼ A)$
90	89	a1i	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to (m \in y ⟼ ⦋ m / n ⦌ A) = (n \in y ⟼ A)$
91	90	oveq2d	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to \underset{m \in y}{\sum_{G}} ⦋ m / n ⦌ A = \underset{n \in y}{\sum_{G}} A$
92		simpr	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to \underset{n \in y}{\sum_{G}} A \neq 0_{R}$
93	91 92	eqnetrd	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to \underset{m \in y}{\sum_{G}} ⦋ m / n ⦌ A \neq 0_{R}$
94	86 93	jca	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to (\underset{m \in y}{\sum_{G}} ⦋ m / n ⦌ A \in {Base}_{R} \land \underset{m \in y}{\sum_{G}} ⦋ m / n ⦌ A \neq 0_{R})$
95	5	ralrimiva	$⊢ φ \to \forall n \in N A \neq 0_{R}$
96	95	adantr	$⊢ (φ \land (y \subseteq N \land z \in (N ∖ y))) \to \forall n \in N A \neq 0_{R}$
97		rspcsbnea	$⊢ (z \in N \land \forall n \in N A \neq 0_{R}) \to ⦋ z / n ⦌ A \neq 0_{R}$
98	68 96 97	syl2anc	$⊢ (φ \land (y \subseteq N \land z \in (N ∖ y))) \to ⦋ z / n ⦌ A \neq 0_{R}$
99	98	adantr	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to ⦋ z / n ⦌ A \neq 0_{R}$
100	76 99	jca	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to (⦋ z / n ⦌ A \in {Base}_{R} \land ⦋ z / n ⦌ A \neq 0_{R})$
101		eqid	$⊢ \cdot_{R} = \cdot_{R}$
102	1 101	mgpplusg	$⊢ \cdot_{R} = +_{G}$
103	102	eqcomi	$⊢ +_{G} = \cdot_{R}$
104	62 103 32	domnmuln0	$⊢ (R \in Domn \land (\underset{m \in y}{\sum_{G}} ⦋ m / n ⦌ A \in {Base}_{R} \land \underset{m \in y}{\sum_{G}} ⦋ m / n ⦌ A \neq 0_{R}) \land (⦋ z / n ⦌ A \in {Base}_{R} \land ⦋ z / n ⦌ A \neq 0_{R})) \to (\underset{m \in y}{\sum_{G}}, ⦋ m / n ⦌ A) +_{G} ⦋ z / n ⦌ A \neq 0_{R}$
105	84 94 100 104	syl3anc	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to (\underset{m \in y}{\sum_{G}}, ⦋ m / n ⦌ A) +_{G} ⦋ z / n ⦌ A \neq 0_{R}$
106	81 105	eqnetrd	$⊢ ((φ \land (y \subseteq N \land z \in (N ∖ y))) \land \underset{n \in y}{\sum_{G}} A \neq 0_{R}) \to \underset{n \in y \cup \{z\}}{\sum_{G}} A \neq 0_{R}$
107	106	ex	$⊢ (φ \land (y \subseteq N \land z \in (N ∖ y))) \to (\underset{n \in y}{\sum_{G}} A \neq 0_{R} \to \underset{n \in y \cup \{z\}}{\sum_{G}} A \neq 0_{R})$
108	8 11 14 17 36 107 3	findcard2d	$⊢ φ \to \underset{n \in N}{\sum_{G}} A \neq 0_{R}$

Metamath Proof Explorer

Theorem idomnnzgmulnz

Proof