This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem domnprodn0

Description: In a domain, a finite product of nonzero terms is nonzero. (Contributed by Thierry Arnoux, 6-Jun-2025)

Ref Expression
Hypotheses domnprodn0.1 
|- B = ( Base ` R )
domnprodn0.2 
|- M = ( mulGrp ` R )
domnprodn0.3 
|- .0. = ( 0g ` R )
domnprodn0.4 
|- ( ph -> R e. Domn )
domnprodn0.5 
|- ( ph -> F e. Word ( B \ { .0. } ) )
Assertion domnprodn0 
|- ( ph -> ( M gsum F ) =/= .0. )

Proof

Step Hyp Ref Expression
1 domnprodn0.1 
 |-  B = ( Base ` R )
2 domnprodn0.2 
 |-  M = ( mulGrp ` R )
3 domnprodn0.3 
 |-  .0. = ( 0g ` R )
4 domnprodn0.4 
 |-  ( ph -> R e. Domn )
5 domnprodn0.5 
 |-  ( ph -> F e. Word ( B \ { .0. } ) )
6 oveq2 
 |-  ( g = (/) -> ( M gsum g ) = ( M gsum (/) ) )
7 6 neeq1d 
 |-  ( g = (/) -> ( ( M gsum g ) =/= .0. <-> ( M gsum (/) ) =/= .0. ) )
8 7 imbi2d 
 |-  ( g = (/) -> ( ( ph -> ( M gsum g ) =/= .0. ) <-> ( ph -> ( M gsum (/) ) =/= .0. ) ) )
9 oveq2 
 |-  ( g = f -> ( M gsum g ) = ( M gsum f ) )
10 9 neeq1d 
 |-  ( g = f -> ( ( M gsum g ) =/= .0. <-> ( M gsum f ) =/= .0. ) )
11 10 imbi2d 
 |-  ( g = f -> ( ( ph -> ( M gsum g ) =/= .0. ) <-> ( ph -> ( M gsum f ) =/= .0. ) ) )
12 oveq2 
 |-  ( g = ( f ++ <" x "> ) -> ( M gsum g ) = ( M gsum ( f ++ <" x "> ) ) )
13 12 neeq1d 
 |-  ( g = ( f ++ <" x "> ) -> ( ( M gsum g ) =/= .0. <-> ( M gsum ( f ++ <" x "> ) ) =/= .0. ) )
14 13 imbi2d 
 |-  ( g = ( f ++ <" x "> ) -> ( ( ph -> ( M gsum g ) =/= .0. ) <-> ( ph -> ( M gsum ( f ++ <" x "> ) ) =/= .0. ) ) )
15 oveq2 
 |-  ( g = F -> ( M gsum g ) = ( M gsum F ) )
16 15 neeq1d 
 |-  ( g = F -> ( ( M gsum g ) =/= .0. <-> ( M gsum F ) =/= .0. ) )
17 16 imbi2d 
 |-  ( g = F -> ( ( ph -> ( M gsum g ) =/= .0. ) <-> ( ph -> ( M gsum F ) =/= .0. ) ) )
18 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
19 2 18 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
20 19 gsum0 
 |-  ( M gsum (/) ) = ( 1r ` R )
21 20 a1i 
 |-  ( ph -> ( M gsum (/) ) = ( 1r ` R ) )
22 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
23 18 3 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= .0. )
24 4 22 23 3syl 
 |-  ( ph -> ( 1r ` R ) =/= .0. )
25 21 24 eqnetrd 
 |-  ( ph -> ( M gsum (/) ) =/= .0. )
26 domnring 
 |-  ( R e. Domn -> R e. Ring )
27 2 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
28 4 26 27 3syl 
 |-  ( ph -> M e. Mnd )
29 28 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) /\ ( M gsum f ) =/= .0. ) -> M e. Mnd )
30 difssd 
 |-  ( ph -> ( B \ { .0. } ) C_ B )
31 sswrd 
 |-  ( ( B \ { .0. } ) C_ B -> Word ( B \ { .0. } ) C_ Word B )
32 30 31 syl 
 |-  ( ph -> Word ( B \ { .0. } ) C_ Word B )
33 32 sselda 
 |-  ( ( ph /\ f e. Word ( B \ { .0. } ) ) -> f e. Word B )
34 33 ad2antrr 
 |-  ( ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) /\ ( M gsum f ) =/= .0. ) -> f e. Word B )
35 simplr 
 |-  ( ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) /\ ( M gsum f ) =/= .0. ) -> x e. ( B \ { .0. } ) )
36 35 eldifad 
 |-  ( ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) /\ ( M gsum f ) =/= .0. ) -> x e. B )
37 2 1 mgpbas 
 |-  B = ( Base ` M )
38 eqid 
 |-  ( .r ` R ) = ( .r ` R )
39 2 38 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
40 37 39 gsumccatsn 
 |-  ( ( M e. Mnd /\ f e. Word B /\ x e. B ) -> ( M gsum ( f ++ <" x "> ) ) = ( ( M gsum f ) ( .r ` R ) x ) )
41 29 34 36 40 syl3anc 
 |-  ( ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) /\ ( M gsum f ) =/= .0. ) -> ( M gsum ( f ++ <" x "> ) ) = ( ( M gsum f ) ( .r ` R ) x ) )
42 4 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) /\ ( M gsum f ) =/= .0. ) -> R e. Domn )
43 37 gsumwcl 
 |-  ( ( M e. Mnd /\ f e. Word B ) -> ( M gsum f ) e. B )
44 29 34 43 syl2anc 
 |-  ( ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) /\ ( M gsum f ) =/= .0. ) -> ( M gsum f ) e. B )
45 simpr 
 |-  ( ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) /\ ( M gsum f ) =/= .0. ) -> ( M gsum f ) =/= .0. )
46 eldifsni 
 |-  ( x e. ( B \ { .0. } ) -> x =/= .0. )
47 35 46 syl 
 |-  ( ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) /\ ( M gsum f ) =/= .0. ) -> x =/= .0. )
48 1 38 3 domnmuln0 
 |-  ( ( R e. Domn /\ ( ( M gsum f ) e. B /\ ( M gsum f ) =/= .0. ) /\ ( x e. B /\ x =/= .0. ) ) -> ( ( M gsum f ) ( .r ` R ) x ) =/= .0. )
49 42 44 45 36 47 48 syl122anc 
 |-  ( ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) /\ ( M gsum f ) =/= .0. ) -> ( ( M gsum f ) ( .r ` R ) x ) =/= .0. )
50 41 49 eqnetrd 
 |-  ( ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) /\ ( M gsum f ) =/= .0. ) -> ( M gsum ( f ++ <" x "> ) ) =/= .0. )
51 50 ex 
 |-  ( ( ( ph /\ f e. Word ( B \ { .0. } ) ) /\ x e. ( B \ { .0. } ) ) -> ( ( M gsum f ) =/= .0. -> ( M gsum ( f ++ <" x "> ) ) =/= .0. ) )
52 51 anasss 
 |-  ( ( ph /\ ( f e. Word ( B \ { .0. } ) /\ x e. ( B \ { .0. } ) ) ) -> ( ( M gsum f ) =/= .0. -> ( M gsum ( f ++ <" x "> ) ) =/= .0. ) )
53 52 expcom 
 |-  ( ( f e. Word ( B \ { .0. } ) /\ x e. ( B \ { .0. } ) ) -> ( ph -> ( ( M gsum f ) =/= .0. -> ( M gsum ( f ++ <" x "> ) ) =/= .0. ) ) )
54 53 a2d 
 |-  ( ( f e. Word ( B \ { .0. } ) /\ x e. ( B \ { .0. } ) ) -> ( ( ph -> ( M gsum f ) =/= .0. ) -> ( ph -> ( M gsum ( f ++ <" x "> ) ) =/= .0. ) ) )
55 8 11 14 17 25 54 wrdind 
 |-  ( F e. Word ( B \ { .0. } ) -> ( ph -> ( M gsum F ) =/= .0. ) )
56 5 55 mpcom 
 |-  ( ph -> ( M gsum F ) =/= .0. )