Metamath Proof Explorer

Theorem idomnnzgmulnz

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

Ref Expression
Hypotheses idomnnzgmulnz.1 
|- G = ( mulGrp ` R )
idomnnzgmulnz.2 
|- ( ph -> R e. IDomn )
idomnnzgmulnz.3 
|- ( ph -> N e. Fin )
idomnnzgmulnz.4 
|- ( ( ph /\ n e. N ) -> A e. ( Base ` R ) )
idomnnzgmulnz.5 
|- ( ( ph /\ n e. N ) -> A =/= ( 0g ` R ) )
Assertion idomnnzgmulnz 
|- ( ph -> ( G gsum ( n e. N |-> A ) ) =/= ( 0g ` R ) )

Proof

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