Theorem 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	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	idomnnzgmulnz.2	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
	idomnnzgmulnz.3	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	idomnnzgmulnz.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
	idomnnzgmulnz.5	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝐴 ≠ ( 0g ‘ 𝑅 ) )
Assertion	idomnnzgmulnz	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		idomnnzgmulnz.1	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
2		idomnnzgmulnz.2	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
3		idomnnzgmulnz.3	⊢ ( 𝜑 → 𝑁 ∈ Fin )
4		idomnnzgmulnz.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
5		idomnnzgmulnz.5	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝐴 ≠ ( 0g ‘ 𝑅 ) )
6		mpteq1	⊢ ( 𝑥 = ∅ → ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) = ( 𝑛 ∈ ∅ ↦ 𝐴 ) )
7	6	oveq2d	⊢ ( 𝑥 = ∅ → ( 𝐺 Σg ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) ) = ( 𝐺 Σg ( 𝑛 ∈ ∅ ↦ 𝐴 ) ) )
8	7	neeq1d	⊢ ( 𝑥 = ∅ → ( ( 𝐺 Σg ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ↔ ( 𝐺 Σg ( 𝑛 ∈ ∅ ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) )
9		mpteq1	⊢ ( 𝑥 = 𝑦 → ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) = ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) )
10	9	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐺 Σg ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) ) = ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) )
11	10	neeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐺 Σg ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ↔ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) )
12		mpteq1	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) = ( 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ 𝐴 ) )
13	12	oveq2d	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) ) = ( 𝐺 Σg ( 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ 𝐴 ) ) )
14	13	neeq1d	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐺 Σg ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ↔ ( 𝐺 Σg ( 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) )
15		mpteq1	⊢ ( 𝑥 = 𝑁 → ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) = ( 𝑛 ∈ 𝑁 ↦ 𝐴 ) )
16	15	oveq2d	⊢ ( 𝑥 = 𝑁 → ( 𝐺 Σg ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) ) = ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ 𝐴 ) ) )
17	16	neeq1d	⊢ ( 𝑥 = 𝑁 → ( ( 𝐺 Σg ( 𝑛 ∈ 𝑥 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ↔ ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) )
18		mpt0	⊢ ( 𝑛 ∈ ∅ ↦ 𝐴 ) = ∅
19	18	a1i	⊢ ( 𝜑 → ( 𝑛 ∈ ∅ ↦ 𝐴 ) = ∅ )
20	19	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑛 ∈ ∅ ↦ 𝐴 ) ) = ( 𝐺 Σg ∅ ) )
21		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
22	21	gsum0	⊢ ( 𝐺 Σg ∅ ) = ( 0g ‘ 𝐺 )
23	22	a1i	⊢ ( 𝜑 → ( 𝐺 Σg ∅ ) = ( 0g ‘ 𝐺 ) )
24	20 23	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑛 ∈ ∅ ↦ 𝐴 ) ) = ( 0g ‘ 𝐺 ) )
25		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
26	1 25	ringidval	⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 )
27	26	eqcomi	⊢ ( 0g ‘ 𝐺 ) = ( 1r ‘ 𝑅 )
28	27	a1i	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) = ( 1r ‘ 𝑅 ) )
29		isidom	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
30	29	simprbi	⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ Domn )
31		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
32		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
33	25 32	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
34	2 30 31 33	4syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
35	28 34	eqnetrd	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ≠ ( 0g ‘ 𝑅 ) )
36	24 35	eqnetrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑛 ∈ ∅ ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) )
37		nfcv	⊢ Ⅎ 𝑚 𝐴
38		nfcsb1v	⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴
39		csbeq1a	⊢ ( 𝑛 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
40	37 38 39	cbvmpt	⊢ ( 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ 𝐴 ) = ( 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
41	40	oveq2i	⊢ ( 𝐺 Σg ( 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ 𝐴 ) ) = ( 𝐺 Σg ( 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
42	41	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ 𝐴 ) ) = ( 𝐺 Σg ( 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) )
43		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
44		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
45	29	simplbi	⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ CRing )
46	2 45	syl	⊢ ( 𝜑 → 𝑅 ∈ CRing )
47	1	crngmgp	⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )
48	46 47	syl	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
49	48	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) → 𝐺 ∈ CMnd )
50	49	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → 𝐺 ∈ CMnd )
51	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) → 𝑁 ∈ Fin )
52		simprl	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) → 𝑦 ⊆ 𝑁 )
53	51 52	ssfid	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) → 𝑦 ∈ Fin )
54	53	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑦 ∈ Fin )
55	52	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑦 ) → 𝑦 ⊆ 𝑁 )
56		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑦 ) → 𝑚 ∈ 𝑦 )
57	55 56	sseldd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑦 ) → 𝑚 ∈ 𝑁 )
58	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑁 𝐴 ∈ ( Base ‘ 𝑅 ) )
59	58	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑦 ) → ∀ 𝑛 ∈ 𝑁 𝐴 ∈ ( Base ‘ 𝑅 ) )
60		rspcsbela	⊢ ( ( 𝑚 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 𝐴 ∈ ( Base ‘ 𝑅 ) ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ( Base ‘ 𝑅 ) )
61	57 59 60	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑦 ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ( Base ‘ 𝑅 ) )
62		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
63	1 62	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 )
64	63	a1i	⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑦 ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 ) )
65	61 64	eleqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) ∧ 𝑚 ∈ 𝑦 ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ( Base ‘ 𝐺 ) )
66		eldifi	⊢ ( 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) → 𝑧 ∈ 𝑁 )
67	66	adantl	⊢ ( ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) → 𝑧 ∈ 𝑁 )
68	67	adantl	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) → 𝑧 ∈ 𝑁 )
69	68	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑧 ∈ 𝑁 )
70		eldifn	⊢ ( 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) → ¬ 𝑧 ∈ 𝑦 )
71	70	adantl	⊢ ( ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) → ¬ 𝑧 ∈ 𝑦 )
72	71	adantl	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) → ¬ 𝑧 ∈ 𝑦 )
73	72	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ¬ 𝑧 ∈ 𝑦 )
74	58	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ∀ 𝑛 ∈ 𝑁 𝐴 ∈ ( Base ‘ 𝑅 ) )
75		rspcsbela	⊢ ( ( 𝑧 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 𝐴 ∈ ( Base ‘ 𝑅 ) ) → ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ∈ ( Base ‘ 𝑅 ) )
76	69 74 75	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ∈ ( Base ‘ 𝑅 ) )
77	63	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 ) )
78	76 77	eleqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ∈ ( Base ‘ 𝐺 ) )
79		csbeq1	⊢ ( 𝑚 = 𝑧 → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 = ⦋ 𝑧 / 𝑛 ⦌ 𝐴 )
80	43 44 50 54 65 69 73 78 79	gsumunsn	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 Σg ( 𝑚 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) = ( ( 𝐺 Σg ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ( +g ‘ 𝐺 ) ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ) )
81	42 80	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ 𝐴 ) ) = ( ( 𝐺 Σg ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ( +g ‘ 𝐺 ) ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ) )
82	2 30	syl	⊢ ( 𝜑 → 𝑅 ∈ Domn )
83	82	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) → 𝑅 ∈ Domn )
84	83	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Domn )
85	61	ralrimiva	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ∀ 𝑚 ∈ 𝑦 ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ( Base ‘ 𝑅 ) )
86	63 50 54 85	gsummptcl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 Σg ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) )
87	39	equcoms	⊢ ( 𝑚 = 𝑛 → 𝐴 = ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
88	87	eqcomd	⊢ ( 𝑚 = 𝑛 → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 = 𝐴 )
89	38 37 88	cbvmpt	⊢ ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) = ( 𝑛 ∈ 𝑦 ↦ 𝐴 )
90	89	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) = ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) )
91	90	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 Σg ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) = ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) )
92		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) )
93	91 92	eqnetrd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 Σg ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) )
94	86 93	jca	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐺 Σg ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 Σg ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) )
95	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑁 𝐴 ≠ ( 0g ‘ 𝑅 ) )
96	95	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) → ∀ 𝑛 ∈ 𝑁 𝐴 ≠ ( 0g ‘ 𝑅 ) )
97		rspcsbnea	⊢ ( ( 𝑧 ∈ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 𝐴 ≠ ( 0g ‘ 𝑅 ) ) → ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ≠ ( 0g ‘ 𝑅 ) )
98	68 96 97	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) → ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ≠ ( 0g ‘ 𝑅 ) )
99	98	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ≠ ( 0g ‘ 𝑅 ) )
100	76 99	jca	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ∈ ( Base ‘ 𝑅 ) ∧ ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ≠ ( 0g ‘ 𝑅 ) ) )
101		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
102	1 101	mgpplusg	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝐺 )
103	102	eqcomi	⊢ ( +g ‘ 𝐺 ) = ( .r ‘ 𝑅 )
104	62 103 32	domnmuln0	⊢ ( ( 𝑅 ∈ Domn ∧ ( ( 𝐺 Σg ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 Σg ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ∈ ( Base ‘ 𝑅 ) ∧ ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐺 Σg ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ( +g ‘ 𝐺 ) ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) )
105	84 94 100 104	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐺 Σg ( 𝑚 ∈ 𝑦 ↦ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) ( +g ‘ 𝐺 ) ⦋ 𝑧 / 𝑛 ⦌ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) )
106	81 105	eqnetrd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) )
107	106	ex	⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑁 ∧ 𝑧 ∈ ( 𝑁 ∖ 𝑦 ) ) ) → ( ( 𝐺 Σg ( 𝑛 ∈ 𝑦 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) → ( 𝐺 Σg ( 𝑛 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) ) )
108	8 11 14 17 36 107 3	findcard2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ 𝐴 ) ) ≠ ( 0g ‘ 𝑅 ) )