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
|- A = { m e. ( NN0 ^m I ) | ( `' m " NN ) e. Fin }
tdeglem.h
|- H = ( h e. A |-> ( CCfld gsum h ) )
Assertion tdeglem4OLD
|- ( ( I e. V /\ 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 ad2antlr
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( H ` X ) = ( CCfld gsum X ) )
9 1 psrbagfOLD
 |-  ( ( I e. V /\ X e. A ) -> X : I --> NN0 )
10 9 feqmptd
 |-  ( ( I e. V /\ X e. A ) -> X = ( y e. I |-> ( X ` y ) ) )
11 10 adantr
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> X = ( y e. I |-> ( X ` y ) ) )
12 11 oveq2d
 |-  ( ( ( I e. V /\ 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
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> CCfld e. CMnd )
19 simpll
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> I e. V )
20 9 adantr
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> X : I --> NN0 )
21 20 ffvelrnda
 |-  ( ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) /\ y e. I ) -> ( X ` y ) e. NN0 )
22 21 nn0cnd
 |-  ( ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) /\ y e. I ) -> ( X ` y ) e. CC )
23 1 psrbagfsuppOLD
 |-  ( ( X e. A /\ I e. V ) -> X finSupp 0 )
24 23 ancoms
 |-  ( ( I e. V /\ X e. A ) -> X finSupp 0 )
25 24 adantr
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> X finSupp 0 )
26 11 25 eqbrtrrd
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( y e. I |-> ( X ` y ) ) finSupp 0 )
27 incom
 |-  ( ( I \ { x } ) i^i { x } ) = ( { x } i^i ( I \ { x } ) )
28 disjdif
 |-  ( { x } i^i ( I \ { x } ) ) = (/)
29 27 28 eqtri
 |-  ( ( I \ { x } ) i^i { x } ) = (/)
30 29 a1i
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( ( I \ { x } ) i^i { x } ) = (/) )
31 difsnid
 |-  ( x e. I -> ( ( I \ { x } ) u. { x } ) = I )
32 31 eqcomd
 |-  ( x e. I -> I = ( ( I \ { x } ) u. { x } ) )
33 32 ad2antrl
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> I = ( ( I \ { x } ) u. { x } ) )
34 13 14 15 18 19 22 26 30 33 gsumsplit2
 |-  ( ( ( I e. V /\ 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 ) ) ) ) )
35 8 12 34 3eqtrd
 |-  ( ( ( I e. V /\ 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 ) ) ) ) )
36 difexg
 |-  ( I e. V -> ( I \ { x } ) e. _V )
37 36 ad2antrr
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( I \ { x } ) e. _V )
38 nn0subm
 |-  NN0 e. ( SubMnd ` CCfld )
39 38 a1i
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> NN0 e. ( SubMnd ` CCfld ) )
40 eldifi
 |-  ( y e. ( I \ { x } ) -> y e. I )
41 ffvelrn
 |-  ( ( X : I --> NN0 /\ y e. I ) -> ( X ` y ) e. NN0 )
42 20 40 41 syl2an
 |-  ( ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) /\ y e. ( I \ { x } ) ) -> ( X ` y ) e. NN0 )
43 42 fmpttd
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( y e. ( I \ { x } ) |-> ( X ` y ) ) : ( I \ { x } ) --> NN0 )
44 36 mptexd
 |-  ( I e. V -> ( y e. ( I \ { x } ) |-> ( X ` y ) ) e. _V )
45 44 ad2antrr
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( y e. ( I \ { x } ) |-> ( X ` y ) ) e. _V )
46 funmpt
 |-  Fun ( y e. ( I \ { x } ) |-> ( X ` y ) )
47 46 a1i
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> Fun ( y e. ( I \ { x } ) |-> ( X ` y ) ) )
48 funmpt
 |-  Fun ( y e. I |-> ( X ` y ) )
49 difss
 |-  ( I \ { x } ) C_ I
50 resmpt
 |-  ( ( I \ { x } ) C_ I -> ( ( y e. I |-> ( X ` y ) ) |` ( I \ { x } ) ) = ( y e. ( I \ { x } ) |-> ( X ` y ) ) )
51 49 50 ax-mp
 |-  ( ( y e. I |-> ( X ` y ) ) |` ( I \ { x } ) ) = ( y e. ( I \ { x } ) |-> ( X ` y ) )
52 resss
 |-  ( ( y e. I |-> ( X ` y ) ) |` ( I \ { x } ) ) C_ ( y e. I |-> ( X ` y ) )
53 51 52 eqsstrri
 |-  ( y e. ( I \ { x } ) |-> ( X ` y ) ) C_ ( y e. I |-> ( X ` y ) )
54 mptexg
 |-  ( I e. V -> ( y e. I |-> ( X ` y ) ) e. _V )
55 54 ad2antrr
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( y e. I |-> ( X ` y ) ) e. _V )
56 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 ) )
57 48 53 55 56 mp3an12i
 |-  ( ( ( I e. V /\ 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 ) )
58 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 )
59 45 47 26 57 58 syl22anc
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( y e. ( I \ { x } ) |-> ( X ` y ) ) finSupp 0 )
60 14 18 37 39 43 59 gsumsubmcl
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( CCfld gsum ( y e. ( I \ { x } ) |-> ( X ` y ) ) ) e. NN0 )
61 ringmnd
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
62 16 61 mp1i
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> CCfld e. Mnd )
63 simprl
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> x e. I )
64 20 63 ffvelrnd
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( X ` x ) e. NN0 )
65 64 nn0cnd
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( X ` x ) e. CC )
66 fveq2
 |-  ( y = x -> ( X ` y ) = ( X ` x ) )
67 13 66 gsumsn
 |-  ( ( CCfld e. Mnd /\ x e. I /\ ( X ` x ) e. CC ) -> ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) = ( X ` x ) )
68 62 63 65 67 syl3anc
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) = ( X ` x ) )
69 simprr
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( X ` x ) =/= 0 )
70 69 4 sylib
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> -. ( X ` x ) = 0 )
71 elnn0
 |-  ( ( X ` x ) e. NN0 <-> ( ( X ` x ) e. NN \/ ( X ` x ) = 0 ) )
72 64 71 sylib
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( ( X ` x ) e. NN \/ ( X ` x ) = 0 ) )
73 orel2
 |-  ( -. ( X ` x ) = 0 -> ( ( ( X ` x ) e. NN \/ ( X ` x ) = 0 ) -> ( X ` x ) e. NN ) )
74 70 72 73 sylc
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( X ` x ) e. NN )
75 68 74 eqeltrd
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( CCfld gsum ( y e. { x } |-> ( X ` y ) ) ) e. NN )
76 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 )
77 60 75 76 syl2anc
 |-  ( ( ( I e. V /\ 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 )
78 77 nnne0d
 |-  ( ( ( I e. V /\ 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 )
79 35 78 eqnetrd
 |-  ( ( ( I e. V /\ X e. A ) /\ ( x e. I /\ ( X ` x ) =/= 0 ) ) -> ( H ` X ) =/= 0 )
80 79 expr
 |-  ( ( ( I e. V /\ X e. A ) /\ x e. I ) -> ( ( X ` x ) =/= 0 -> ( H ` X ) =/= 0 ) )
81 4 80 syl5bir
 |-  ( ( ( I e. V /\ X e. A ) /\ x e. I ) -> ( -. ( X ` x ) = 0 -> ( H ` X ) =/= 0 ) )
82 81 rexlimdva
 |-  ( ( I e. V /\ X e. A ) -> ( E. x e. I -. ( X ` x ) = 0 -> ( H ` X ) =/= 0 ) )
83 3 82 syl5bir
 |-  ( ( I e. V /\ X e. A ) -> ( -. A. x e. I ( X ` x ) = 0 -> ( H ` X ) =/= 0 ) )
84 83 necon4bd
 |-  ( ( I e. V /\ X e. A ) -> ( ( H ` X ) = 0 -> A. x e. I ( X ` x ) = 0 ) )
85 9 ffnd
 |-  ( ( I e. V /\ X e. A ) -> X Fn I )
86 0nn0
 |-  0 e. NN0
87 fnconstg
 |-  ( 0 e. NN0 -> ( I X. { 0 } ) Fn I )
88 86 87 mp1i
 |-  ( ( I e. V /\ X e. A ) -> ( I X. { 0 } ) Fn I )
89 eqfnfv
 |-  ( ( X Fn I /\ ( I X. { 0 } ) Fn I ) -> ( X = ( I X. { 0 } ) <-> A. x e. I ( X ` x ) = ( ( I X. { 0 } ) ` x ) ) )
90 85 88 89 syl2anc
 |-  ( ( I e. V /\ X e. A ) -> ( X = ( I X. { 0 } ) <-> A. x e. I ( X ` x ) = ( ( I X. { 0 } ) ` x ) ) )
91 c0ex
 |-  0 e. _V
92 91 fvconst2
 |-  ( x e. I -> ( ( I X. { 0 } ) ` x ) = 0 )
93 92 eqeq2d
 |-  ( x e. I -> ( ( X ` x ) = ( ( I X. { 0 } ) ` x ) <-> ( X ` x ) = 0 ) )
94 93 ralbiia
 |-  ( A. x e. I ( X ` x ) = ( ( I X. { 0 } ) ` x ) <-> A. x e. I ( X ` x ) = 0 )
95 90 94 bitrdi
 |-  ( ( I e. V /\ X e. A ) -> ( X = ( I X. { 0 } ) <-> A. x e. I ( X ` x ) = 0 ) )
96 84 95 sylibrd
 |-  ( ( I e. V /\ X e. A ) -> ( ( H ` X ) = 0 -> X = ( I X. { 0 } ) ) )
97 1 psrbag0
 |-  ( I e. V -> ( I X. { 0 } ) e. A )
98 97 adantr
 |-  ( ( I e. V /\ X e. A ) -> ( I X. { 0 } ) e. A )
99 oveq2
 |-  ( h = ( I X. { 0 } ) -> ( CCfld gsum h ) = ( CCfld gsum ( I X. { 0 } ) ) )
100 ovex
 |-  ( CCfld gsum ( I X. { 0 } ) ) e. _V
101 99 2 100 fvmpt
 |-  ( ( I X. { 0 } ) e. A -> ( H ` ( I X. { 0 } ) ) = ( CCfld gsum ( I X. { 0 } ) ) )
102 98 101 syl
 |-  ( ( I e. V /\ X e. A ) -> ( H ` ( I X. { 0 } ) ) = ( CCfld gsum ( I X. { 0 } ) ) )
103 fconstmpt
 |-  ( I X. { 0 } ) = ( x e. I |-> 0 )
104 103 oveq2i
 |-  ( CCfld gsum ( I X. { 0 } ) ) = ( CCfld gsum ( x e. I |-> 0 ) )
105 16 61 ax-mp
 |-  CCfld e. Mnd
106 14 gsumz
 |-  ( ( CCfld e. Mnd /\ I e. V ) -> ( CCfld gsum ( x e. I |-> 0 ) ) = 0 )
107 105 106 mpan
 |-  ( I e. V -> ( CCfld gsum ( x e. I |-> 0 ) ) = 0 )
108 107 adantr
 |-  ( ( I e. V /\ X e. A ) -> ( CCfld gsum ( x e. I |-> 0 ) ) = 0 )
109 104 108 syl5eq
 |-  ( ( I e. V /\ X e. A ) -> ( CCfld gsum ( I X. { 0 } ) ) = 0 )
110 102 109 eqtrd
 |-  ( ( I e. V /\ X e. A ) -> ( H ` ( I X. { 0 } ) ) = 0 )
111 fveqeq2
 |-  ( X = ( I X. { 0 } ) -> ( ( H ` X ) = 0 <-> ( H ` ( I X. { 0 } ) ) = 0 ) )
112 110 111 syl5ibrcom
 |-  ( ( I e. V /\ X e. A ) -> ( X = ( I X. { 0 } ) -> ( H ` X ) = 0 ) )
113 96 112 impbid
 |-  ( ( I e. V /\ X e. A ) -> ( ( H ` X ) = 0 <-> X = ( I X. { 0 } ) ) )