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 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
domnprodeq0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
domnprodeq0.1 ⊢ 0 = ( 0g ‘ 𝑅 )
domnprodeq0.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
domnprodeq0.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
domnprodeq0.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion domnprodeq0 ( 𝜑 → ( ( 𝑀 Σg 𝐹 ) = 0 ↔ 0 ∈ ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 domnprodeq0.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2 domnprodeq0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 domnprodeq0.1 ⊢ 0 = ( 0g ‘ 𝑅 )
4 domnprodeq0.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
5 domnprodeq0.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
6 domnprodeq0.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 mpteq1 ⊢ ( 𝑎 = ∅ → ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) )
8 mpt0 ⊢ ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) = ∅
9 7 8 eqtrdi ⊢ ( 𝑎 = ∅ → ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ∅ )
10 9 oveq2d ⊢ ( 𝑎 = ∅ → ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑀 Σg ∅ ) )
11 10 eqeq1d ⊢ ( 𝑎 = ∅ → ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ ( 𝑀 Σg ∅ ) = 0 ) )
12 9 rneqd ⊢ ( 𝑎 = ∅ → ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ran ∅ )
13 12 eleq2d ⊢ ( 𝑎 = ∅ → ( 0 ∈ ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ↔ 0 ∈ ran ∅ ) )
14 11 13 bibi12d ⊢ ( 𝑎 = ∅ → ( ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ↔ ( ( 𝑀 Σg ∅ ) = 0 ↔ 0 ∈ ran ∅ ) ) )
15 mpteq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) )
16 15 oveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
17 16 eqeq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ) )
18 15 rneqd ⊢ ( 𝑎 = 𝑏 → ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) )
19 18 eleq2d ⊢ ( 𝑎 = 𝑏 → ( 0 ∈ ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ↔ 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
20 17 19 bibi12d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ↔ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) )
21 mpteq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑙 } ) → ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) )
22 21 oveq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑙 } ) → ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
23 22 eqeq1d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑙 } ) → ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ) )
24 21 rneqd ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑙 } ) → ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ran ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) )
25 24 eleq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑙 } ) → ( 0 ∈ ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ↔ 0 ∈ ran ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
26 23 25 bibi12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑙 } ) → ( ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ↔ ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) )
27 mpteq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
28 27 oveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
29 28 eqeq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ) )
30 27 rneqd ⊢ ( 𝑎 = 𝐴 → ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
31 30 eleq2d ⊢ ( 𝑎 = 𝐴 → ( 0 ∈ ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ↔ 0 ∈ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
32 29 31 bibi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑀 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ↔ ( ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) )
33 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
34 1 33 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
35 34 gsum0 ⊢ ( 𝑀 Σg ∅ ) = ( 1r ‘ 𝑅 )
36 35 a1i ⊢ ( 𝜑 → ( 𝑀 Σg ∅ ) = ( 1r ‘ 𝑅 ) )
37 4 idomdomd ⊢ ( 𝜑 → 𝑅 ∈ Domn )
38 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
39 33 3 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
40 37 38 39 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ 0 )
41 36 40 eqnetrd ⊢ ( 𝜑 → ( 𝑀 Σg ∅ ) ≠ 0 )
42 41 neneqd ⊢ ( 𝜑 → ¬ ( 𝑀 Σg ∅ ) = 0 )
43 noel ⊢ ¬ 0 ∈ ∅
44 rn0 ⊢ ran ∅ = ∅
45 44 eleq2i ⊢ ( 0 ∈ ran ∅ ↔ 0 ∈ ∅ )
46 43 45 mtbir ⊢ ¬ 0 ∈ ran ∅
47 46 a1i ⊢ ( 𝜑 → ¬ 0 ∈ ran ∅ )
48 42 47 2falsed ⊢ ( 𝜑 → ( ( 𝑀 Σg ∅ ) = 0 ↔ 0 ∈ ran ∅ ) )
49 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
50 49 orbi1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ∨ ( 𝐹 ‘ 𝑙 ) = 0 ) ↔ ( 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ∨ ( 𝐹 ‘ 𝑙 ) = 0 ) ) )
51 1 2 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑀 )
52 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
53 1 52 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
54 4 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
55 1 crngmgp ⊢ ( 𝑅 ∈ CRing → 𝑀 ∈ CMnd )
56 54 55 syl ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
57 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑀 ∈ CMnd )
58 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝐴 ∈ Fin )
59 simplr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑏 ⊆ 𝐴 )
60 58 59 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑏 ∈ Fin )
61 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
62 59 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝑘 ∈ 𝐴 )
63 61 62 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑘 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )
64 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) )
65 64 eldifbd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → ¬ 𝑙 ∈ 𝑏 )
66 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
67 64 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑙 ∈ 𝐴 )
68 66 67 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝐹 ‘ 𝑙 ) ∈ 𝐵 )
69 fveq2 ⊢ ( 𝑘 = 𝑙 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑙 ) )
70 51 53 57 60 63 64 65 68 69 gsumunsn ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑙 ) ) )
71 70 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑙 ) ) = 0 ) )
72 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑅 ∈ Domn )
73 63 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → ∀ 𝑘 ∈ 𝑏 ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )
74 51 57 60 73 gsummptcl ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ 𝐵 )
75 2 52 3 domneq0 ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝐵 ) → ( ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑙 ) ) = 0 ↔ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ∨ ( 𝐹 ‘ 𝑙 ) = 0 ) ) )
76 72 74 68 75 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑙 ) ) = 0 ↔ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ∨ ( 𝐹 ‘ 𝑙 ) = 0 ) ) )
77 71 76 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ∨ ( 𝐹 ‘ 𝑙 ) = 0 ) ) )
78 77 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ∨ ( 𝐹 ‘ 𝑙 ) = 0 ) ) )
79 eqid ⊢ ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) )
80 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
81 79 80 elrnmpti ⊢ ( 0 ∈ ran ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ↔ ∃ 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) 0 = ( 𝐹 ‘ 𝑘 ) )
82 rexun ⊢ ( ∃ 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) 0 = ( 𝐹 ‘ 𝑘 ) ↔ ( ∃ 𝑘 ∈ 𝑏 0 = ( 𝐹 ‘ 𝑘 ) ∨ ∃ 𝑘 ∈ { 𝑙 } 0 = ( 𝐹 ‘ 𝑘 ) ) )
83 eqid ⊢ ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) )
84 83 80 elrnmpti ⊢ ( 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ↔ ∃ 𝑘 ∈ 𝑏 0 = ( 𝐹 ‘ 𝑘 ) )
85 84 bicomi ⊢ ( ∃ 𝑘 ∈ 𝑏 0 = ( 𝐹 ‘ 𝑘 ) ↔ 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) )
86 vex ⊢ 𝑙 ∈ V
87 69 eqeq2d ⊢ ( 𝑘 = 𝑙 → ( 0 = ( 𝐹 ‘ 𝑘 ) ↔ 0 = ( 𝐹 ‘ 𝑙 ) ) )
88 eqcom ⊢ ( 0 = ( 𝐹 ‘ 𝑙 ) ↔ ( 𝐹 ‘ 𝑙 ) = 0 )
89 87 88 bitrdi ⊢ ( 𝑘 = 𝑙 → ( 0 = ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑙 ) = 0 ) )
90 86 89 rexsn ⊢ ( ∃ 𝑘 ∈ { 𝑙 } 0 = ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑙 ) = 0 )
91 85 90 orbi12i ⊢ ( ( ∃ 𝑘 ∈ 𝑏 0 = ( 𝐹 ‘ 𝑘 ) ∨ ∃ 𝑘 ∈ { 𝑙 } 0 = ( 𝐹 ‘ 𝑘 ) ) ↔ ( 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ∨ ( 𝐹 ‘ 𝑙 ) = 0 ) )
92 81 82 91 3bitri ⊢ ( 0 ∈ ran ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ↔ ( 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ∨ ( 𝐹 ‘ 𝑙 ) = 0 ) )
93 92 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( 0 ∈ ran ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ↔ ( 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ∨ ( 𝐹 ‘ 𝑙 ) = 0 ) ) )
94 50 78 93 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) → ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
95 94 ex ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) )
96 95 anasss ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( ( 𝑀 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) → ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ ( 𝑏 ∪ { 𝑙 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) )
97 14 20 26 32 48 96 5 findcard2d ⊢ ( 𝜑 → ( ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ↔ 0 ∈ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
98 6 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
99 98 oveq2d ⊢ ( 𝜑 → ( 𝑀 Σg 𝐹 ) = ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
100 99 eqeq1d ⊢ ( 𝜑 → ( ( 𝑀 Σg 𝐹 ) = 0 ↔ ( 𝑀 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 ) )
101 98 rneqd ⊢ ( 𝜑 → ran 𝐹 = ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
102 101 eleq2d ⊢ ( 𝜑 → ( 0 ∈ ran 𝐹 ↔ 0 ∈ ran ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
103 97 100 102 3bitr4d ⊢ ( 𝜑 → ( ( 𝑀 Σg 𝐹 ) = 0 ↔ 0 ∈ ran 𝐹 ) )