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

Metamath Proof Explorer

Theorem domnprodeq0

Description: A product over a domain is zero exactly when one of the factors is zero. Generalization of domneq0 for any number of factors. See also domnprodn0 . (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses domnprodeq0.m 
|- M = ( mulGrp ` R )
domnprodeq0.b 
|- B = ( Base ` R )
domnprodeq0.1 
|- .0. = ( 0g ` R )
domnprodeq0.r 
|- ( ph -> R e. IDomn )
domnprodeq0.2 
|- ( ph -> A e. Fin )
domnprodeq0.f 
|- ( ph -> F : A --> B )
Assertion domnprodeq0 
|- ( ph -> ( ( M gsum F ) = .0. <-> .0. e. ran F ) )

Proof

Step Hyp Ref Expression
1 domnprodeq0.m 
 |-  M = ( mulGrp ` R )
2 domnprodeq0.b 
 |-  B = ( Base ` R )
3 domnprodeq0.1 
 |-  .0. = ( 0g ` R )
4 domnprodeq0.r 
 |-  ( ph -> R e. IDomn )
5 domnprodeq0.2 
 |-  ( ph -> A e. Fin )
6 domnprodeq0.f 
 |-  ( ph -> F : A --> B )
7 mpteq1 
 |-  ( a = (/) -> ( k e. a |-> ( F ` k ) ) = ( k e. (/) |-> ( F ` k ) ) )
8 mpt0 
 |-  ( k e. (/) |-> ( F ` k ) ) = (/)
9 7 8 eqtrdi 
 |-  ( a = (/) -> ( k e. a |-> ( F ` k ) ) = (/) )
10 9 oveq2d 
 |-  ( a = (/) -> ( M gsum ( k e. a |-> ( F ` k ) ) ) = ( M gsum (/) ) )
11 10 eqeq1d 
 |-  ( a = (/) -> ( ( M gsum ( k e. a |-> ( F ` k ) ) ) = .0. <-> ( M gsum (/) ) = .0. ) )
12 9 rneqd 
 |-  ( a = (/) -> ran ( k e. a |-> ( F ` k ) ) = ran (/) )
13 12 eleq2d 
 |-  ( a = (/) -> ( .0. e. ran ( k e. a |-> ( F ` k ) ) <-> .0. e. ran (/) ) )
14 11 13 bibi12d 
 |-  ( a = (/) -> ( ( ( M gsum ( k e. a |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. a |-> ( F ` k ) ) ) <-> ( ( M gsum (/) ) = .0. <-> .0. e. ran (/) ) ) )
15 mpteq1 
 |-  ( a = b -> ( k e. a |-> ( F ` k ) ) = ( k e. b |-> ( F ` k ) ) )
16 15 oveq2d 
 |-  ( a = b -> ( M gsum ( k e. a |-> ( F ` k ) ) ) = ( M gsum ( k e. b |-> ( F ` k ) ) ) )
17 16 eqeq1d 
 |-  ( a = b -> ( ( M gsum ( k e. a |-> ( F ` k ) ) ) = .0. <-> ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. ) )
18 15 rneqd 
 |-  ( a = b -> ran ( k e. a |-> ( F ` k ) ) = ran ( k e. b |-> ( F ` k ) ) )
19 18 eleq2d 
 |-  ( a = b -> ( .0. e. ran ( k e. a |-> ( F ` k ) ) <-> .0. e. ran ( k e. b |-> ( F ` k ) ) ) )
20 17 19 bibi12d 
 |-  ( a = b -> ( ( ( M gsum ( k e. a |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. a |-> ( F ` k ) ) ) <-> ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. b |-> ( F ` k ) ) ) ) )
21 mpteq1 
 |-  ( a = ( b u. { l } ) -> ( k e. a |-> ( F ` k ) ) = ( k e. ( b u. { l } ) |-> ( F ` k ) ) )
22 21 oveq2d 
 |-  ( a = ( b u. { l } ) -> ( M gsum ( k e. a |-> ( F ` k ) ) ) = ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) )
23 22 eqeq1d 
 |-  ( a = ( b u. { l } ) -> ( ( M gsum ( k e. a |-> ( F ` k ) ) ) = .0. <-> ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) = .0. ) )
24 21 rneqd 
 |-  ( a = ( b u. { l } ) -> ran ( k e. a |-> ( F ` k ) ) = ran ( k e. ( b u. { l } ) |-> ( F ` k ) ) )
25 24 eleq2d 
 |-  ( a = ( b u. { l } ) -> ( .0. e. ran ( k e. a |-> ( F ` k ) ) <-> .0. e. ran ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) )
26 23 25 bibi12d 
 |-  ( a = ( b u. { l } ) -> ( ( ( M gsum ( k e. a |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. a |-> ( F ` k ) ) ) <-> ( ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) ) )
27 mpteq1 
 |-  ( a = A -> ( k e. a |-> ( F ` k ) ) = ( k e. A |-> ( F ` k ) ) )
28 27 oveq2d 
 |-  ( a = A -> ( M gsum ( k e. a |-> ( F ` k ) ) ) = ( M gsum ( k e. A |-> ( F ` k ) ) ) )
29 28 eqeq1d 
 |-  ( a = A -> ( ( M gsum ( k e. a |-> ( F ` k ) ) ) = .0. <-> ( M gsum ( k e. A |-> ( F ` k ) ) ) = .0. ) )
30 27 rneqd 
 |-  ( a = A -> ran ( k e. a |-> ( F ` k ) ) = ran ( k e. A |-> ( F ` k ) ) )
31 30 eleq2d 
 |-  ( a = A -> ( .0. e. ran ( k e. a |-> ( F ` k ) ) <-> .0. e. ran ( k e. A |-> ( F ` k ) ) ) )
32 29 31 bibi12d 
 |-  ( a = A -> ( ( ( M gsum ( k e. a |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. a |-> ( F ` k ) ) ) <-> ( ( M gsum ( k e. A |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. A |-> ( F ` k ) ) ) ) )
33 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
34 1 33 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
35 34 gsum0 
 |-  ( M gsum (/) ) = ( 1r ` R )
36 35 a1i 
 |-  ( ph -> ( M gsum (/) ) = ( 1r ` R ) )
37 4 idomdomd 
 |-  ( ph -> R e. Domn )
38 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
39 33 3 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= .0. )
40 37 38 39 3syl 
 |-  ( ph -> ( 1r ` R ) =/= .0. )
41 36 40 eqnetrd 
 |-  ( ph -> ( M gsum (/) ) =/= .0. )
42 41 neneqd 
 |-  ( ph -> -. ( M gsum (/) ) = .0. )
43 noel 
 |-  -. .0. e. (/)
44 rn0 
 |-  ran (/) = (/)
45 44 eleq2i 
 |-  ( .0. e. ran (/) <-> .0. e. (/) )
46 43 45 mtbir 
 |-  -. .0. e. ran (/)
47 46 a1i 
 |-  ( ph -> -. .0. e. ran (/) )
48 42 47 2falsed 
 |-  ( ph -> ( ( M gsum (/) ) = .0. <-> .0. e. ran (/) ) )
49 simpr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. b |-> ( F ` k ) ) ) ) -> ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. b |-> ( F ` k ) ) ) )
50 49 orbi1d 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. b |-> ( F ` k ) ) ) ) -> ( ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. \/ ( F ` l ) = .0. ) <-> ( .0. e. ran ( k e. b |-> ( F ` k ) ) \/ ( F ` l ) = .0. ) ) )
51 1 2 mgpbas 
 |-  B = ( Base ` M )
52 eqid 
 |-  ( .r ` R ) = ( .r ` R )
53 1 52 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
54 4 idomcringd 
 |-  ( ph -> R e. CRing )
55 1 crngmgp 
 |-  ( R e. CRing -> M e. CMnd )
56 54 55 syl 
 |-  ( ph -> M e. CMnd )
57 56 ad2antrr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> M e. CMnd )
58 5 ad2antrr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> A e. Fin )
59 simplr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> b C_ A )
60 58 59 ssfid 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> b e. Fin )
61 6 ad3antrrr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ k e. b ) -> F : A --> B )
62 59 sselda 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ k e. b ) -> k e. A )
63 61 62 ffvelcdmd 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ k e. b ) -> ( F ` k ) e. B )
64 simpr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> l e. ( A \ b ) )
65 64 eldifbd 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> -. l e. b )
66 6 ad2antrr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> F : A --> B )
67 64 eldifad 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> l e. A )
68 66 67 ffvelcdmd 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( F ` l ) e. B )
69 fveq2 
 |-  ( k = l -> ( F ` k ) = ( F ` l ) )
70 51 53 57 60 63 64 65 68 69 gsumunsn 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) = ( ( M gsum ( k e. b |-> ( F ` k ) ) ) ( .r ` R ) ( F ` l ) ) )
71 70 eqeq1d 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) = .0. <-> ( ( M gsum ( k e. b |-> ( F ` k ) ) ) ( .r ` R ) ( F ` l ) ) = .0. ) )
72 37 ad2antrr 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> R e. Domn )
73 63 ralrimiva 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> A. k e. b ( F ` k ) e. B )
74 51 57 60 73 gsummptcl 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( M gsum ( k e. b |-> ( F ` k ) ) ) e. B )
75 2 52 3 domneq0 
 |-  ( ( R e. Domn /\ ( M gsum ( k e. b |-> ( F ` k ) ) ) e. B /\ ( F ` l ) e. B ) -> ( ( ( M gsum ( k e. b |-> ( F ` k ) ) ) ( .r ` R ) ( F ` l ) ) = .0. <-> ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. \/ ( F ` l ) = .0. ) ) )
76 72 74 68 75 syl3anc 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( ( ( M gsum ( k e. b |-> ( F ` k ) ) ) ( .r ` R ) ( F ` l ) ) = .0. <-> ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. \/ ( F ` l ) = .0. ) ) )
77 71 76 bitrd 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) = .0. <-> ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. \/ ( F ` l ) = .0. ) ) )
78 77 adantr 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. b |-> ( F ` k ) ) ) ) -> ( ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) = .0. <-> ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. \/ ( F ` l ) = .0. ) ) )
79 eqid 
 |-  ( k e. ( b u. { l } ) |-> ( F ` k ) ) = ( k e. ( b u. { l } ) |-> ( F ` k ) )
80 fvex 
 |-  ( F ` k ) e. _V
81 79 80 elrnmpti 
 |-  ( .0. e. ran ( k e. ( b u. { l } ) |-> ( F ` k ) ) <-> E. k e. ( b u. { l } ) .0. = ( F ` k ) )
82 rexun 
 |-  ( E. k e. ( b u. { l } ) .0. = ( F ` k ) <-> ( E. k e. b .0. = ( F ` k ) \/ E. k e. { l } .0. = ( F ` k ) ) )
83 eqid 
 |-  ( k e. b |-> ( F ` k ) ) = ( k e. b |-> ( F ` k ) )
84 83 80 elrnmpti 
 |-  ( .0. e. ran ( k e. b |-> ( F ` k ) ) <-> E. k e. b .0. = ( F ` k ) )
85 84 bicomi 
 |-  ( E. k e. b .0. = ( F ` k ) <-> .0. e. ran ( k e. b |-> ( F ` k ) ) )
86 vex 
 |-  l e. _V
87 69 eqeq2d 
 |-  ( k = l -> ( .0. = ( F ` k ) <-> .0. = ( F ` l ) ) )
88 eqcom 
 |-  ( .0. = ( F ` l ) <-> ( F ` l ) = .0. )
89 87 88 bitrdi 
 |-  ( k = l -> ( .0. = ( F ` k ) <-> ( F ` l ) = .0. ) )
90 86 89 rexsn 
 |-  ( E. k e. { l } .0. = ( F ` k ) <-> ( F ` l ) = .0. )
91 85 90 orbi12i 
 |-  ( ( E. k e. b .0. = ( F ` k ) \/ E. k e. { l } .0. = ( F ` k ) ) <-> ( .0. e. ran ( k e. b |-> ( F ` k ) ) \/ ( F ` l ) = .0. ) )
92 81 82 91 3bitri 
 |-  ( .0. e. ran ( k e. ( b u. { l } ) |-> ( F ` k ) ) <-> ( .0. e. ran ( k e. b |-> ( F ` k ) ) \/ ( F ` l ) = .0. ) )
93 92 a1i 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. b |-> ( F ` k ) ) ) ) -> ( .0. e. ran ( k e. ( b u. { l } ) |-> ( F ` k ) ) <-> ( .0. e. ran ( k e. b |-> ( F ` k ) ) \/ ( F ` l ) = .0. ) ) )
94 50 78 93 3bitr4d 
 |-  ( ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) /\ ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. b |-> ( F ` k ) ) ) ) -> ( ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) )
95 94 ex 
 |-  ( ( ( ph /\ b C_ A ) /\ l e. ( A \ b ) ) -> ( ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. b |-> ( F ` k ) ) ) -> ( ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) ) )
96 95 anasss 
 |-  ( ( ph /\ ( b C_ A /\ l e. ( A \ b ) ) ) -> ( ( ( M gsum ( k e. b |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. b |-> ( F ` k ) ) ) -> ( ( M gsum ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. ( b u. { l } ) |-> ( F ` k ) ) ) ) )
97 14 20 26 32 48 96 5 findcard2d 
 |-  ( ph -> ( ( M gsum ( k e. A |-> ( F ` k ) ) ) = .0. <-> .0. e. ran ( k e. A |-> ( F ` k ) ) ) )
98 6 feqmptd 
 |-  ( ph -> F = ( k e. A |-> ( F ` k ) ) )
99 98 oveq2d 
 |-  ( ph -> ( M gsum F ) = ( M gsum ( k e. A |-> ( F ` k ) ) ) )
100 99 eqeq1d 
 |-  ( ph -> ( ( M gsum F ) = .0. <-> ( M gsum ( k e. A |-> ( F ` k ) ) ) = .0. ) )
101 98 rneqd 
 |-  ( ph -> ran F = ran ( k e. A |-> ( F ` k ) ) )
102 101 eleq2d 
 |-  ( ph -> ( .0. e. ran F <-> .0. e. ran ( k e. A |-> ( F ` k ) ) ) )
103 97 100 102 3bitr4d 
 |-  ( ph -> ( ( M gsum F ) = .0. <-> .0. e. ran F ) )