Metamath Proof Explorer

Theorem tdeglem4OLD

Description: Obsolete version of tdeglem4 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 29-Mar-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses tdeglem.a ⊢ 𝐴 = { 𝑚 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑚 “ ℕ ) ∈ Fin }
tdeglem.h ⊢ 𝐻 = ( ℎ ∈ 𝐴 ↦ ( ℂfld Σg ℎ ) )
Assertion tdeglem4OLD ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑋 ) = 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 ad2antlr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐻 ‘ 𝑋 ) = ( ℂfld Σg 𝑋 ) )
9 1 psrbagfOLD ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 : 𝐼 ⟶ ℕ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 simpll ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → 𝐼 ∈ 𝑉 )
20 9 adantr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → 𝑋 : 𝐼 ⟶ ℕ0 )
21 20 ffvelrnda ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑦 ) ∈ ℕ0 )
22 21 nn0cnd ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑦 ) ∈ ℂ )
23 1 psrbagfsuppOLD ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐼 ∈ 𝑉 ) → 𝑋 finSupp 0 )
24 23 ancoms ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 finSupp 0 )
25 24 adantr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → 𝑋 finSupp 0 )
26 11 25 eqbrtrrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) finSupp 0 )
27 incom ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ( { 𝑥 } ∩ ( 𝐼 ∖ { 𝑥 } ) )
28 disjdif ⊢ ( { 𝑥 } ∩ ( 𝐼 ∖ { 𝑥 } ) ) = ∅
29 27 28 eqtri ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅
30 29 a1i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ( 𝐼 ∖ { 𝑥 } ) ∩ { 𝑥 } ) = ∅ )
31 difsnid ⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝐼 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = 𝐼 )
32 31 eqcomd ⊢ ( 𝑥 ∈ 𝐼 → 𝐼 = ( ( 𝐼 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
33 32 ad2antrl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → 𝐼 = ( ( 𝐼 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
34 13 14 15 18 19 22 26 30 33 gsumsplit2 ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ℂfld Σg ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ) = ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) + ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ) )
35 8 12 34 3eqtrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐻 ‘ 𝑋 ) = ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) + ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ) )
36 difexg ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 ∖ { 𝑥 } ) ∈ V )
37 36 ad2antrr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐼 ∖ { 𝑥 } ) ∈ V )
38 nn0subm ⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
39 38 a1i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ℕ0 ∈ ( SubMnd ‘ ℂfld ) )
40 eldifi ⊢ ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) → 𝑦 ∈ 𝐼 )
41 ffvelrn ⊢ ( ( 𝑋 : 𝐼 ⟶ ℕ0 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑦 ) ∈ ℕ0 )
42 20 40 41 syl2an ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) ∧ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ) → ( 𝑋 ‘ 𝑦 ) ∈ ℕ0 )
43 42 fmpttd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) : ( 𝐼 ∖ { 𝑥 } ) ⟶ ℕ0 )
44 36 mptexd ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ∈ V )
45 44 ad2antrr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ∈ V )
46 funmpt ⊢ Fun ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) )
47 46 a1i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → Fun ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) )
48 funmpt ⊢ Fun ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) )
49 difss ⊢ ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼
50 resmpt ⊢ ( ( 𝐼 ∖ { 𝑥 } ) ⊆ 𝐼 → ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ↾ ( 𝐼 ∖ { 𝑥 } ) ) = ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) )
51 49 50 ax-mp ⊢ ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ↾ ( 𝐼 ∖ { 𝑥 } ) ) = ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) )
52 resss ⊢ ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ↾ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) )
53 51 52 eqsstrri ⊢ ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ⊆ ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) )
54 mptexg ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ∈ V )
55 54 ad2antrr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ∈ V )
56 funsssuppss ⊢ ( ( Fun ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ⊆ ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) ∈ V ) → ( ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) ⊆ ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) )
57 48 53 55 56 mp3an12i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) ⊆ ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) )
58 fsuppsssupp ⊢ ( ( ( ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ∈ V ∧ Fun ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) ∧ ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) finSupp 0 ∧ ( ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) ⊆ ( ( 𝑦 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑦 ) ) supp 0 ) ) ) → ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) finSupp 0 )
59 45 47 26 57 58 syl22anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) finSupp 0 )
60 14 18 37 39 43 59 gsumsubmcl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) ∈ ℕ0 )
61 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
62 16 61 mp1i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ℂfld ∈ Mnd )
63 simprl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → 𝑥 ∈ 𝐼 )
64 20 63 ffvelrnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℕ0 )
65 64 nn0cnd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
66 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑋 ‘ 𝑦 ) = ( 𝑋 ‘ 𝑥 ) )
67 13 66 gsumsn ⊢ ( ( ℂfld ∈ Mnd ∧ 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ∈ ℂ ) → ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) = ( 𝑋 ‘ 𝑥 ) )
68 62 63 65 67 syl3anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) = ( 𝑋 ‘ 𝑥 ) )
69 simprr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑋 ‘ 𝑥 ) ≠ 0 )
70 69 4 sylib ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ¬ ( 𝑋 ‘ 𝑥 ) = 0 )
71 elnn0 ⊢ ( ( 𝑋 ‘ 𝑥 ) ∈ ℕ0 ↔ ( ( 𝑋 ‘ 𝑥 ) ∈ ℕ ∨ ( 𝑋 ‘ 𝑥 ) = 0 ) )
72 64 71 sylib ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ( 𝑋 ‘ 𝑥 ) ∈ ℕ ∨ ( 𝑋 ‘ 𝑥 ) = 0 ) )
73 orel2 ⊢ ( ¬ ( 𝑋 ‘ 𝑥 ) = 0 → ( ( ( 𝑋 ‘ 𝑥 ) ∈ ℕ ∨ ( 𝑋 ‘ 𝑥 ) = 0 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℕ ) )
74 70 72 73 sylc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℕ )
75 68 74 eqeltrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ∈ ℕ )
76 nn0nnaddcl ⊢ ( ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) ∈ ℕ0 ∧ ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ∈ ℕ ) → ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) + ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ) ∈ ℕ )
77 60 75 76 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) + ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ) ∈ ℕ )
78 77 nnne0d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ℂfld Σg ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↦ ( 𝑋 ‘ 𝑦 ) ) ) + ( ℂfld Σg ( 𝑦 ∈ { 𝑥 } ↦ ( 𝑋 ‘ 𝑦 ) ) ) ) ≠ 0 )
79 35 78 eqnetrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐻 ‘ 𝑋 ) ≠ 0 )
80 79 expr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → ( 𝐻 ‘ 𝑋 ) ≠ 0 ) )
81 4 80 syl5bir ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐼 ) → ( ¬ ( 𝑋 ‘ 𝑥 ) = 0 → ( 𝐻 ‘ 𝑋 ) ≠ 0 ) )
82 81 rexlimdva ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐼 ¬ ( 𝑋 ‘ 𝑥 ) = 0 → ( 𝐻 ‘ 𝑋 ) ≠ 0 ) )
83 3 82 syl5bir ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ¬ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = 0 → ( 𝐻 ‘ 𝑋 ) ≠ 0 ) )
84 83 necon4bd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑋 ) = 0 → ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = 0 ) )
85 9 ffnd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 Fn 𝐼 )
86 0nn0 ⊢ 0 ∈ ℕ0
87 fnconstg ⊢ ( 0 ∈ ℕ0 → ( 𝐼 × { 0 } ) Fn 𝐼 )
88 86 87 mp1i ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐼 × { 0 } ) Fn 𝐼 )
89 eqfnfv ⊢ ( ( 𝑋 Fn 𝐼 ∧ ( 𝐼 × { 0 } ) Fn 𝐼 ) → ( 𝑋 = ( 𝐼 × { 0 } ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) ) )
90 85 88 89 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 = ( 𝐼 × { 0 } ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) ) )
91 c0ex ⊢ 0 ∈ V
92 91 fvconst2 ⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) = 0 )
93 92 eqeq2d ⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝑋 ‘ 𝑥 ) = ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) ↔ ( 𝑋 ‘ 𝑥 ) = 0 ) )
94 93 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = ( ( 𝐼 × { 0 } ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = 0 )
95 90 94 bitrdi ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 = ( 𝐼 × { 0 } ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑋 ‘ 𝑥 ) = 0 ) )
96 84 95 sylibrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑋 ) = 0 → 𝑋 = ( 𝐼 × { 0 } ) ) )
97 1 psrbag0 ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × { 0 } ) ∈ 𝐴 )
98 97 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐼 × { 0 } ) ∈ 𝐴 )
99 oveq2 ⊢ ( ℎ = ( 𝐼 × { 0 } ) → ( ℂfld Σg ℎ ) = ( ℂfld Σg ( 𝐼 × { 0 } ) ) )
100 ovex ⊢ ( ℂfld Σg ( 𝐼 × { 0 } ) ) ∈ V
101 99 2 100 fvmpt ⊢ ( ( 𝐼 × { 0 } ) ∈ 𝐴 → ( 𝐻 ‘ ( 𝐼 × { 0 } ) ) = ( ℂfld Σg ( 𝐼 × { 0 } ) ) )
102 98 101 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝐼 × { 0 } ) ) = ( ℂfld Σg ( 𝐼 × { 0 } ) ) )
103 fconstmpt ⊢ ( 𝐼 × { 0 } ) = ( 𝑥 ∈ 𝐼 ↦ 0 )
104 103 oveq2i ⊢ ( ℂfld Σg ( 𝐼 × { 0 } ) ) = ( ℂfld Σg ( 𝑥 ∈ 𝐼 ↦ 0 ) )
105 16 61 ax-mp ⊢ ℂfld ∈ Mnd
106 14 gsumz ⊢ ( ( ℂfld ∈ Mnd ∧ 𝐼 ∈ 𝑉 ) → ( ℂfld Σg ( 𝑥 ∈ 𝐼 ↦ 0 ) ) = 0 )
107 105 106 mpan ⊢ ( 𝐼 ∈ 𝑉 → ( ℂfld Σg ( 𝑥 ∈ 𝐼 ↦ 0 ) ) = 0 )
108 107 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ℂfld Σg ( 𝑥 ∈ 𝐼 ↦ 0 ) ) = 0 )
109 104 108 eqtrid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ℂfld Σg ( 𝐼 × { 0 } ) ) = 0 )
110 102 109 eqtrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝐼 × { 0 } ) ) = 0 )
111 fveqeq2 ⊢ ( 𝑋 = ( 𝐼 × { 0 } ) → ( ( 𝐻 ‘ 𝑋 ) = 0 ↔ ( 𝐻 ‘ ( 𝐼 × { 0 } ) ) = 0 ) )
112 110 111 syl5ibrcom ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 = ( 𝐼 × { 0 } ) → ( 𝐻 ‘ 𝑋 ) = 0 ) )
113 96 112 impbid ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑋 ) = 0 ↔ 𝑋 = ( 𝐼 × { 0 } ) ) )