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 
|- A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
tdeglem.h 
|- H = ( h e. A |-> ( CCfld gsum h ) )
Assertion tdeglem4 
|- ( X e. A -> ( ( H ` X ) = 0 <-> X = ( I X. { 0 } ) ) )

Proof

Step Hyp Ref Expression
1 tdeglem.a 
 |-  A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
2 tdeglem.h 
 |-  H = ( h e. A |-> ( CCfld gsum h ) )
3 rexnal 
 |-  ( E. x e. I -. ( X ` x ) = 0 <-> -. A. x e. I ( X ` x ) = 0 )
4 df-ne 
 |-  ( ( X ` x ) =/= 0 <-> -. ( X ` x ) = 0 )
5 oveq2 
 |-  ( h = X -> ( CCfld gsum h ) = ( CCfld gsum X ) )
6 ovex 
 |-  ( CCfld gsum X ) e. _V
7 5 2 6 fvmpt 
 |-  ( X e. A -> ( H ` X ) = ( CCfld gsum X ) )
8 7 adantr 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( H ` X ) = ( CCfld gsum X ) )
9 1 psrbagf 
 |-  ( X e. A -> X : I --> NN0 )
10 9 feqmptd 
 |-  ( X e. A -> X = ( y e. I |-> ( X ` y ) ) )
11 10 adantr 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> X = ( y e. I |-> ( X ` y ) ) )
12 11 oveq2d 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( CCfld gsum X ) = ( CCfld gsum ( y e. I |-> ( X ` y ) ) ) )
13 cnfldbas 
 |-  CC = ( Base ` CCfld )
14 cnfld0 
 |-  0 = ( 0g ` CCfld )
15 cnfldadd 
 |-  + = ( +g ` CCfld )
16 cnring 
 |-  CCfld e. Ring
17 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
18 16 17 mp1i 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> CCfld e. CMnd )
19 id 
 |-  ( X e. A -> X e. A )
20 9 ffnd 
 |-  ( X e. A -> X Fn I )
21 19 20 fndmexd 
 |-  ( X e. A -> I e. _V )
22 21 adantr 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> I e. _V )
23 9 ffvelrnda 
 |-  ( ( X e. A /\ y e. I ) -> ( X ` y ) e. NN0 )
24 23 nn0cnd 
 |-  ( ( X e. A /\ y e. I ) -> ( X ` y ) e. CC )
25 24 adantlr 
 |-  ( ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) /\ y e. I ) -> ( X ` y ) e. CC )
26 1 psrbagfsupp 
 |-  ( X e. A -> X finSupp 0 )
27 10 26 eqbrtrrd 
 |-  ( X e. A -> ( y e. I |-> ( X ` y ) ) finSupp 0 )
28 27 adantr 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( y e. I |-> ( X ` y ) ) finSupp 0 )
29 incom 
 |-  ( ( I \ { x } ) i^i { x } ) = ( { x } i^i ( I \ { x } ) )
30 disjdif 
 |-  ( { x } i^i ( I \ { x } ) ) = (/)
31 29 30 eqtri 
 |-  ( ( I \ { x } ) i^i { x } ) = (/)
32 31 a1i 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( ( I \ { x } ) i^i { x } ) = (/) )
33 difsnid 
 |-  ( x e. I -> ( ( I \ { x } ) u. { x } ) = I )
34 33 eqcomd 
 |-  ( x e. I -> I = ( ( I \ { x } ) u. { x } ) )
35 34 ad2antrl 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> I = ( ( I \ { x } ) u. { x } ) )
36 13 14 15 18 22 25 28 32 35 gsumsplit2 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( CCfld gsum ( y e. I |-> ( X ` y ) ) ) = ( ( CCfld gsum ( y e. ( I \ { x } ) |-> ( X ` y ) ) ) + ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) ) )
37 8 12 36 3eqtrd 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( H ` X ) = ( ( CCfld gsum ( y e. ( I \ { x } ) |-> ( X ` y ) ) ) + ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) ) )
38 difexg 
 |-  ( I e. _V -> ( I \ { x } ) e. _V )
39 22 38 syl 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( I \ { x } ) e. _V )
40 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
41 40 a1i 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> NN0 e. ( SubMnd ` CCfld ) )
42 9 adantr 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> X : I --> NN0 )
43 eldifi 
 |-  ( y e. ( I \ { x } ) -> y e. I )
44 ffvelrn 
 |-  ( ( X : I --> NN0 /\ y e. I ) -> ( X ` y ) e. NN0 )
45 42 43 44 syl2an 
 |-  ( ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) /\ y e. ( I \ { x } ) ) -> ( X ` y ) e. NN0 )
46 45 fmpttd 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( y e. ( I \ { x } ) |-> ( X ` y ) ) : ( I \ { x } ) --> NN0 )
47 39 mptexd 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( y e. ( I \ { x } ) |-> ( X ` y ) ) e. _V )
48 funmpt 
 |-  Fun ( y e. ( I \ { x } ) |-> ( X ` y ) )
49 48 a1i 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> Fun ( y e. ( I \ { x } ) |-> ( X ` y ) ) )
50 funmpt 
 |-  Fun ( y e. I |-> ( X ` y ) )
51 difss 
 |-  ( I \ { x } ) C_ I
52 mptss 
 |-  ( ( I \ { x } ) C_ I -> ( y e. ( I \ { x } ) |-> ( X ` y ) ) C_ ( y e. I |-> ( X ` y ) ) )
53 51 52 ax-mp 
 |-  ( y e. ( I \ { x } ) |-> ( X ` y ) ) C_ ( y e. I |-> ( X ` y ) )
54 22 mptexd 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( y e. I |-> ( X ` y ) ) e. _V )
55 funsssuppss 
 |-  ( ( Fun ( y e. I |-> ( X ` y ) ) /\ ( y e. ( I \ { x } ) |-> ( X ` y ) ) C_ ( y e. I |-> ( X ` y ) ) /\ ( y e. I |-> ( X ` y ) ) e. _V ) -> ( ( y e. ( I \ { x } ) |-> ( X ` y ) ) supp 0 ) C_ ( ( y e. I |-> ( X ` y ) ) supp 0 ) )
56 50 53 54 55 mp3an12i 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( ( y e. ( I \ { x } ) |-> ( X ` y ) ) supp 0 ) C_ ( ( y e. I |-> ( X ` y ) ) supp 0 ) )
57 fsuppsssupp 
 |-  ( ( ( ( y e. ( I \ { x } ) |-> ( X ` y ) ) e. _V /\ Fun ( y e. ( I \ { x } ) |-> ( X ` y ) ) ) /\ ( ( y e. I |-> ( X ` y ) ) finSupp 0 /\ ( ( y e. ( I \ { x } ) |-> ( X ` y ) ) supp 0 ) C_ ( ( y e. I |-> ( X ` y ) ) supp 0 ) ) ) -> ( y e. ( I \ { x } ) |-> ( X ` y ) ) finSupp 0 )
58 47 49 28 56 57 syl22anc 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( y e. ( I \ { x } ) |-> ( X ` y ) ) finSupp 0 )
59 14 18 39 41 46 58 gsumsubmcl 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( CCfld gsum ( y e. ( I \ { x } ) |-> ( X ` y ) ) ) e. NN0 )
60 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
61 16 60 ax-mp 
 |-  CCfld e. Mnd
62 simprl 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> x e. I )
63 42 62 ffvelrnd 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( X ` x ) e. NN0 )
64 63 nn0cnd 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( X ` x ) e. CC )
65 fveq2 
 |-  ( y = x -> ( X ` y ) = ( X ` x ) )
66 13 65 gsumsn 
 |-  ( ( CCfld e. Mnd /\ x e. I /\ ( X ` x ) e. CC ) -> ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) = ( X ` x ) )
67 61 62 64 66 mp3an2i 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) = ( X ` x ) )
68 elnn0 
 |-  ( ( X ` x ) e. NN0 <-> ( ( X ` x ) e. NN \/ ( X ` x ) = 0 ) )
69 63 68 sylib 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( ( X ` x ) e. NN \/ ( X ` x ) = 0 ) )
70 neneq 
 |-  ( ( X ` x ) =/= 0 -> -. ( X ` x ) = 0 )
71 70 ad2antll 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> -. ( X ` x ) = 0 )
72 69 71 olcnd 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( X ` x ) e. NN )
73 67 72 eqeltrd 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) e. NN )
74 nn0nnaddcl 
 |-  ( ( ( CCfld gsum ( y e. ( I \ { x } ) |-> ( X ` y ) ) ) e. NN0 /\ ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) e. NN ) -> ( ( CCfld gsum ( y e. ( I \ { x } ) |-> ( X ` y ) ) ) + ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) ) e. NN )
75 59 73 74 syl2anc 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( ( CCfld gsum ( y e. ( I \ { x } ) |-> ( X ` y ) ) ) + ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) ) e. NN )
76 75 nnne0d 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( ( CCfld gsum ( y e. ( I \ { x } ) |-> ( X ` y ) ) ) + ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) ) =/= 0 )
77 37 76 eqnetrd 
 |-  ( ( X e. A /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( H ` X ) =/= 0 )
78 77 expr 
 |-  ( ( X e. A /\ x e. I ) -> ( ( X ` x ) =/= 0 -> ( H ` X ) =/= 0 ) )
79 4 78 syl5bir 
 |-  ( ( X e. A /\ x e. I ) -> ( -. ( X ` x ) = 0 -> ( H ` X ) =/= 0 ) )
80 79 rexlimdva 
 |-  ( X e. A -> ( E. x e. I -. ( X ` x ) = 0 -> ( H ` X ) =/= 0 ) )
81 3 80 syl5bir 
 |-  ( X e. A -> ( -. A. x e. I ( X ` x ) = 0 -> ( H ` X ) =/= 0 ) )
82 81 necon4bd 
 |-  ( X e. A -> ( ( H ` X ) = 0 -> A. x e. I ( X ` x ) = 0 ) )
83 c0ex 
 |-  0 e. _V
84 fnconstg 
 |-  ( 0 e. _V -> ( I X. { 0 } ) Fn I )
85 83 84 mp1i 
 |-  ( X e. A -> ( I X. { 0 } ) Fn I )
86 eqfnfv 
 |-  ( ( X Fn I /\ ( I X. { 0 } ) Fn I ) -> ( X = ( I X. { 0 } ) <-> A. x e. I ( X ` x ) = ( ( I X. { 0 } ) ` x ) ) )
87 20 85 86 syl2anc 
 |-  ( X e. A -> ( X = ( I X. { 0 } ) <-> A. x e. I ( X ` x ) = ( ( I X. { 0 } ) ` x ) ) )
88 83 fvconst2 
 |-  ( x e. I -> ( ( I X. { 0 } ) ` x ) = 0 )
89 88 eqeq2d 
 |-  ( x e. I -> ( ( X ` x ) = ( ( I X. { 0 } ) ` x ) <-> ( X ` x ) = 0 ) )
90 89 ralbiia 
 |-  ( A. x e. I ( X ` x ) = ( ( I X. { 0 } ) ` x ) <-> A. x e. I ( X ` x ) = 0 )
91 87 90 bitrdi 
 |-  ( X e. A -> ( X = ( I X. { 0 } ) <-> A. x e. I ( X ` x ) = 0 ) )
92 82 91 sylibrd 
 |-  ( X e. A -> ( ( H ` X ) = 0 -> X = ( I X. { 0 } ) ) )
93 1 psrbag0 
 |-  ( I e. _V -> ( I X. { 0 } ) e. A )
94 oveq2 
 |-  ( h = ( I X. { 0 } ) -> ( CCfld gsum h ) = ( CCfld gsum ( I X. { 0 } ) ) )
95 ovex 
 |-  ( CCfld gsum ( I X. { 0 } ) ) e. _V
96 94 2 95 fvmpt 
 |-  ( ( I X. { 0 } ) e. A -> ( H ` ( I X. { 0 } ) ) = ( CCfld gsum ( I X. { 0 } ) ) )
97 21 93 96 3syl 
 |-  ( X e. A -> ( H ` ( I X. { 0 } ) ) = ( CCfld gsum ( I X. { 0 } ) ) )
98 fconstmpt 
 |-  ( I X. { 0 } ) = ( x e. I |-> 0 )
99 98 oveq2i 
 |-  ( CCfld gsum ( I X. { 0 } ) ) = ( CCfld gsum ( x e. I |-> 0 ) )
100 14 gsumz 
 |-  ( ( CCfld e. Mnd /\ I e. _V ) -> ( CCfld gsum ( x e. I |-> 0 ) ) = 0 )
101 61 21 100 sylancr 
 |-  ( X e. A -> ( CCfld gsum ( x e. I |-> 0 ) ) = 0 )
102 99 101 syl5eq 
 |-  ( X e. A -> ( CCfld gsum ( I X. { 0 } ) ) = 0 )
103 97 102 eqtrd 
 |-  ( X e. A -> ( H ` ( I X. { 0 } ) ) = 0 )
104 fveqeq2 
 |-  ( X = ( I X. { 0 } ) -> ( ( H ` X ) = 0 <-> ( H ` ( I X. { 0 } ) ) = 0 ) )
105 103 104 syl5ibrcom 
 |-  ( X e. A -> ( X = ( I X. { 0 } ) -> ( H ` X ) = 0 ) )
106 92 105 impbid 
 |-  ( X e. A -> ( ( H ` X ) = 0 <-> X = ( I X. { 0 } ) ) )