Metamath Proof Explorer

Theorem tdeglem4

Description: There is only one multi-index with total degree 0. (Contributed by Stefan O'Rear, 29-Mar-2015) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024)

Ref Expression
Hypotheses tdeglem.a ⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
tdeglem.h ⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
Assertion tdeglem4 ( 𝑋 ∈ 𝐴 → ( ( 𝐻 ‘ 𝑋 ) = 0 ↔ 𝑋 = ( 𝐼 × { 0 } ) ) )

Proof

Step Hyp Ref Expression
1 tdeglem.a ⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
2 tdeglem.h ⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
3 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐼 ¬ ( 𝑋 ‘ 𝑥 ) = 0 ↔ ¬ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = 0 )
4 df-ne ⊢ ( ( 𝑋 ‘ 𝑥 ) ≠ 0 ↔ ¬ ( 𝑋 ‘ 𝑥 ) = 0 )
5 oveq2 ⊢ ( ℎ = 𝑋 → ( ℂfld Σg ℎ ) = ( ℂfld Σg 𝑋 ) )
6 ovex ⊢ ( ℂfld Σg 𝑋 ) ∈ V
7 5 2 6 fvmpt ⊢ ( 𝑋 ∈ 𝐴 → ( 𝐻 ‘ 𝑋 ) = ( ℂfld Σg 𝑋 ) )
8 7 adantr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐻 ‘ 𝑋 ) = ( ℂfld Σg 𝑋 ) )
9 1 psrbagf ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 : 𝐼 ⟶ ℕ0 )
10 9 feqmptd ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) )
11 10 adantr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → 𝑋 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) )
12 11 oveq2d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ℂfld Σg 𝑋 ) = ( ℂfld Σg ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ) )
13 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
14 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
15 cnfldadd ⊢ + = ( +g ‘ ℂfld )
16 cnring ⊢ ℂfld ∈ Ring
17 ringcmn ⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
18 16 17 mp1i ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ℂfld ∈ CMnd )
19 id ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐴 )
20 9 ffnd ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 Fn 𝐼 )
21 19 20 fndmexd ⊢ ( 𝑋 ∈ 𝐴 → 𝐼 ∈ V )
22 21 adantr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → 𝐼 ∈ V )
23 9 ffvelrnda ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑦 ) ∈ ℕ0 )
24 23 nn0cnd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑦 ) ∈ ℂ )
25 24 adantlr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑦 ) ∈ ℂ )
26 1 psrbagfsupp ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 finSupp 0 )
27 10 26 eqbrtrrd ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) finSupp 0 )
28 27 adantr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) finSupp 0 )
29 incom ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ( { 𝑥 } ∩ ( 𝐼 ∖ { 𝑥 } ) )
30 disjdif ⊢ ( { 𝑥 } ∩ ( 𝐼 ∖ { 𝑥 } ) ) = ∅
31 29 30 eqtri ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅
32 31 a1i ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ( 𝐼 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ )
33 difsnid ⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝐼 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = 𝐼 )
34 33 eqcomd ⊢ ( 𝑥 ∈ 𝐼 → 𝐼 = ( ( 𝐼 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
35 34 ad2antrl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → 𝐼 = ( ( 𝐼 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
36 13 14 15 18 22 25 28 32 35 gsumsplit2 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ℂfld Σg ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ) = ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) + ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ) )
37 8 12 36 3eqtrd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐻 ‘ 𝑋 ) = ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) + ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ) )
38 difexg ⊢ ( 𝐼 ∈ V → ( 𝐼 ∖ { 𝑥 } ) ∈ V )
39 22 38 syl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐼 ∖ { 𝑥 } ) ∈ V )
40 nn0subm ⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
41 40 a1i ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ℕ0 ∈ ( SubMnd ‘ ℂfld ) )
42 9 adantr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → 𝑋 : 𝐼 ⟶ ℕ0 )
43 eldifi ⊢ ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) → 𝑦 ∈ 𝐼 )
44 ffvelrn ⊢ ( ( 𝑋 : 𝐼 ⟶ ℕ0 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑦 ) ∈ ℕ0 )
45 42 43 44 syl2an ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) ∧ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ) → ( 𝑋 ‘ 𝑦 ) ∈ ℕ0 )
46 45 fmpttd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) : ( 𝐼 ∖ { 𝑥 } ) ⟶ ℕ0 )
47 39 mptexd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ∈ V )
48 funmpt ⊢ Fun ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) )
49 48 a1i ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → Fun ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) )
50 funmpt ⊢ Fun ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) )
51 difss ⊢ ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼
52 mptss ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼 → ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ⊆ ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) )
53 51 52 ax-mp ⊢ ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ⊆ ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) )
54 22 mptexd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ∈ V )
55 funsssuppss ⊢ ( ( Fun ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ⊆ ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ∈ V ) → ( ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) ⊆ ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) )
56 50 53 54 55 mp3an12i ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) ⊆ ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) )
57 fsuppsssupp ⊢ ( ( ( ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ∈ V ∧ Fun ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) ∧ ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) finSupp 0 ∧ ( ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) ⊆ ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) ) ) → ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) finSupp 0 )
58 47 49 28 56 57 syl22anc ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) finSupp 0 )
59 14 18 39 41 46 58 gsumsubmcl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) ∈ ℕ0 )
60 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
61 16 60 ax-mp ⊢ ℂfld ∈ Mnd
62 simprl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → 𝑥 ∈ 𝐼 )
63 42 62 ffvelrnd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℕ0 )
64 63 nn0cnd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
65 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑋 ‘ 𝑦 ) = ( 𝑋 ‘ 𝑥 ) )
66 13 65 gsumsn ⊢ ( ( ℂfld ∈ Mnd ∧ 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ∈ ℂ ) → ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) = ( 𝑋 ‘ 𝑥 ) )
67 61 62 64 66 mp3an2i ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) = ( 𝑋 ‘ 𝑥 ) )
68 elnn0 ⊢ ( ( 𝑋 ‘ 𝑥 ) ∈ ℕ0 ↔ ( ( 𝑋 ‘ 𝑥 ) ∈ ℕ ∨ ( 𝑋 ‘ 𝑥 ) = 0 ) )
69 63 68 sylib ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ( 𝑋 ‘ 𝑥 ) ∈ ℕ ∨ ( 𝑋 ‘ 𝑥 ) = 0 ) )
70 neneq ⊢ ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → ¬ ( 𝑋 ‘ 𝑥 ) = 0 )
71 70 ad2antll ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ¬ ( 𝑋 ‘ 𝑥 ) = 0 )
72 69 71 olcnd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℕ )
73 67 72 eqeltrd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ∈ ℕ )
74 nn0nnaddcl ⊢ ( ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) ∈ ℕ0 ∧ ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ∈ ℕ ) → ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) + ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ) ∈ ℕ )
75 59 73 74 syl2anc ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) + ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ) ∈ ℕ )
76 75 nnne0d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) + ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ) ≠ 0 )
77 37 76 eqnetrd ⊢ ( ( 𝑋 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐻 ‘ 𝑋 ) ≠ 0 )
78 77 expr ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → ( 𝐻 ‘ 𝑋 ) ≠ 0 ) )
79 4 78 syl5bir ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑥 ∈ 𝐼 ) → ( ¬ ( 𝑋 ‘ 𝑥 ) = 0 → ( 𝐻 ‘ 𝑋 ) ≠ 0 ) )
80 79 rexlimdva ⊢ ( 𝑋 ∈ 𝐴 → ( ∃ 𝑥 ∈ 𝐼 ¬ ( 𝑋 ‘ 𝑥 ) = 0 → ( 𝐻 ‘ 𝑋 ) ≠ 0 ) )
81 3 80 syl5bir ⊢ ( 𝑋 ∈ 𝐴 → ( ¬ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = 0 → ( 𝐻 ‘ 𝑋 ) ≠ 0 ) )
82 81 necon4bd ⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐻 ‘ 𝑋 ) = 0 → ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = 0 ) )
83 c0ex ⊢ 0 ∈ V
84 fnconstg ⊢ ( 0 ∈ V → ( 𝐼 × { 0 } ) Fn 𝐼 )
85 83 84 mp1i ⊢ ( 𝑋 ∈ 𝐴 → ( 𝐼 × { 0 } ) Fn 𝐼 )
86 eqfnfv ⊢ ( ( 𝑋 Fn 𝐼 ∧ ( 𝐼 × { 0 } ) Fn 𝐼 ) → ( 𝑋 = ( 𝐼 × { 0 } ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) ) )
87 20 85 86 syl2anc ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 = ( 𝐼 × { 0 } ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) ) )
88 83 fvconst2 ⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) = 0 )
89 88 eqeq2d ⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝑋 ‘ 𝑥 ) = ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) ↔ ( 𝑋 ‘ 𝑥 ) = 0 ) )
90 89 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = 0 )
91 87 90 bitrdi ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 = ( 𝐼 × { 0 } ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = 0 ) )
92 82 91 sylibrd ⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐻 ‘ 𝑋 ) = 0 → 𝑋 = ( 𝐼 × { 0 } ) ) )
93 1 psrbag0 ⊢ ( 𝐼 ∈ V → ( 𝐼 × { 0 } ) ∈ 𝐴 )
94 oveq2 ⊢ ( ℎ = ( 𝐼 × { 0 } ) → ( ℂfld Σg ℎ ) = ( ℂfld Σg ( 𝐼 × { 0 } ) ) )
95 ovex ⊢ ( ℂfld Σg ( 𝐼 × { 0 } ) ) ∈ V
96 94 2 95 fvmpt ⊢ ( ( 𝐼 × { 0 } ) ∈ 𝐴 → ( 𝐻 ‘ ( 𝐼 × { 0 } ) ) = ( ℂfld Σg ( 𝐼 × { 0 } ) ) )
97 21 93 96 3syl ⊢ ( 𝑋 ∈ 𝐴 → ( 𝐻 ‘ ( 𝐼 × { 0 } ) ) = ( ℂfld Σg ( 𝐼 × { 0 } ) ) )
98 fconstmpt ⊢ ( 𝐼 × { 0 } ) = ( 𝑥 ∈ 𝐼 ↦ 0 )
99 98 oveq2i ⊢ ( ℂfld Σg ( 𝐼 × { 0 } ) ) = ( ℂfld Σg ( 𝑥 ∈ 𝐼 ↦ 0 ) )
100 14 gsumz ⊢ ( ( ℂfld ∈ Mnd ∧ 𝐼 ∈ V ) → ( ℂfld Σg ( 𝑥 ∈ 𝐼 ↦ 0 ) ) = 0 )
101 61 21 100 sylancr ⊢ ( 𝑋 ∈ 𝐴 → ( ℂfld Σg ( 𝑥 ∈ 𝐼 ↦ 0 ) ) = 0 )
102 99 101 syl5eq ⊢ ( 𝑋 ∈ 𝐴 → ( ℂfld Σg ( 𝐼 × { 0 } ) ) = 0 )
103 97 102 eqtrd ⊢ ( 𝑋 ∈ 𝐴 → ( 𝐻 ‘ ( 𝐼 × { 0 } ) ) = 0 )
104 fveqeq2 ⊢ ( 𝑋 = ( 𝐼 × { 0 } ) → ( ( 𝐻 ‘ 𝑋 ) = 0 ↔ ( 𝐻 ‘ ( 𝐼 × { 0 } ) ) = 0 ) )
105 103 104 syl5ibrcom ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 = ( 𝐼 × { 0 } ) → ( 𝐻 ‘ 𝑋 ) = 0 ) )
106 92 105 impbid ⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐻 ‘ 𝑋 ) = 0 ↔ 𝑋 = ( 𝐼 × { 0 } ) ) )