Metamath Proof Explorer


Theorem jensen

Description: Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses jensen.1 φ D
jensen.2 φ F : D
jensen.3 φ a D b D a b D
jensen.4 φ A Fin
jensen.5 φ T : A 0 +∞
jensen.6 φ X : A D
jensen.7 φ 0 < fld T
jensen.8 φ x D y D t 0 1 F t x + 1 t y t F x + 1 t F y
Assertion jensen φ fld T × f X fld T D F fld T × f X fld T fld T × f F X fld T

Proof

Step Hyp Ref Expression
1 jensen.1 φ D
2 jensen.2 φ F : D
3 jensen.3 φ a D b D a b D
4 jensen.4 φ A Fin
5 jensen.5 φ T : A 0 +∞
6 jensen.6 φ X : A D
7 jensen.7 φ 0 < fld T
8 jensen.8 φ x D y D t 0 1 F t x + 1 t y t F x + 1 t F y
9 5 ffnd φ T Fn A
10 fnresdm T Fn A T A = T
11 9 10 syl φ T A = T
12 11 oveq2d φ fld T A = fld T
13 7 12 breqtrrd φ 0 < fld T A
14 ssid A A
15 13 14 jctil φ A A 0 < fld T A
16 sseq1 a = a A A
17 reseq2 a = T a = T
18 res0 T =
19 17 18 eqtrdi a = T a =
20 19 oveq2d a = fld T a = fld
21 cnfld0 0 = 0 fld
22 21 gsum0 fld = 0
23 20 22 eqtrdi a = fld T a = 0
24 23 breq2d a = 0 < fld T a 0 < 0
25 16 24 anbi12d a = a A 0 < fld T a A 0 < 0
26 reseq2 a = T × f X a = T × f X
27 26 oveq2d a = fld T × f X a = fld T × f X
28 27 23 oveq12d a = fld T × f X a fld T a = fld T × f X 0
29 reseq2 a = T × f F X a = T × f F X
30 29 oveq2d a = fld T × f F X a = fld T × f F X
31 30 23 oveq12d a = fld T × f F X a fld T a = fld T × f F X 0
32 31 breq2d a = F w fld T × f F X a fld T a F w fld T × f F X 0
33 32 rabbidv a = w D | F w fld T × f F X a fld T a = w D | F w fld T × f F X 0
34 28 33 eleq12d a = fld T × f X a fld T a w D | F w fld T × f F X a fld T a fld T × f X 0 w D | F w fld T × f F X 0
35 25 34 imbi12d a = a A 0 < fld T a fld T × f X a fld T a w D | F w fld T × f F X a fld T a A 0 < 0 fld T × f X 0 w D | F w fld T × f F X 0
36 35 imbi2d a = φ a A 0 < fld T a fld T × f X a fld T a w D | F w fld T × f F X a fld T a φ A 0 < 0 fld T × f X 0 w D | F w fld T × f F X 0
37 sseq1 a = k a A k A
38 reseq2 a = k T a = T k
39 38 oveq2d a = k fld T a = fld T k
40 39 breq2d a = k 0 < fld T a 0 < fld T k
41 37 40 anbi12d a = k a A 0 < fld T a k A 0 < fld T k
42 reseq2 a = k T × f X a = T × f X k
43 42 oveq2d a = k fld T × f X a = fld T × f X k
44 43 39 oveq12d a = k fld T × f X a fld T a = fld T × f X k fld T k
45 reseq2 a = k T × f F X a = T × f F X k
46 45 oveq2d a = k fld T × f F X a = fld T × f F X k
47 46 39 oveq12d a = k fld T × f F X a fld T a = fld T × f F X k fld T k
48 47 breq2d a = k F w fld T × f F X a fld T a F w fld T × f F X k fld T k
49 48 rabbidv a = k w D | F w fld T × f F X a fld T a = w D | F w fld T × f F X k fld T k
50 44 49 eleq12d a = k fld T × f X a fld T a w D | F w fld T × f F X a fld T a fld T × f X k fld T k w D | F w fld T × f F X k fld T k
51 41 50 imbi12d a = k a A 0 < fld T a fld T × f X a fld T a w D | F w fld T × f F X a fld T a k A 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k
52 51 imbi2d a = k φ a A 0 < fld T a fld T × f X a fld T a w D | F w fld T × f F X a fld T a φ k A 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k
53 sseq1 a = k c a A k c A
54 reseq2 a = k c T a = T k c
55 54 oveq2d a = k c fld T a = fld T k c
56 55 breq2d a = k c 0 < fld T a 0 < fld T k c
57 53 56 anbi12d a = k c a A 0 < fld T a k c A 0 < fld T k c
58 reseq2 a = k c T × f X a = T × f X k c
59 58 oveq2d a = k c fld T × f X a = fld T × f X k c
60 59 55 oveq12d a = k c fld T × f X a fld T a = fld T × f X k c fld T k c
61 reseq2 a = k c T × f F X a = T × f F X k c
62 61 oveq2d a = k c fld T × f F X a = fld T × f F X k c
63 62 55 oveq12d a = k c fld T × f F X a fld T a = fld T × f F X k c fld T k c
64 63 breq2d a = k c F w fld T × f F X a fld T a F w fld T × f F X k c fld T k c
65 64 rabbidv a = k c w D | F w fld T × f F X a fld T a = w D | F w fld T × f F X k c fld T k c
66 60 65 eleq12d a = k c fld T × f X a fld T a w D | F w fld T × f F X a fld T a fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
67 57 66 imbi12d a = k c a A 0 < fld T a fld T × f X a fld T a w D | F w fld T × f F X a fld T a k c A 0 < fld T k c fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
68 67 imbi2d a = k c φ a A 0 < fld T a fld T × f X a fld T a w D | F w fld T × f F X a fld T a φ k c A 0 < fld T k c fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
69 sseq1 a = A a A A A
70 reseq2 a = A T a = T A
71 70 oveq2d a = A fld T a = fld T A
72 71 breq2d a = A 0 < fld T a 0 < fld T A
73 69 72 anbi12d a = A a A 0 < fld T a A A 0 < fld T A
74 reseq2 a = A T × f X a = T × f X A
75 74 oveq2d a = A fld T × f X a = fld T × f X A
76 75 71 oveq12d a = A fld T × f X a fld T a = fld T × f X A fld T A
77 reseq2 a = A T × f F X a = T × f F X A
78 77 oveq2d a = A fld T × f F X a = fld T × f F X A
79 78 71 oveq12d a = A fld T × f F X a fld T a = fld T × f F X A fld T A
80 79 breq2d a = A F w fld T × f F X a fld T a F w fld T × f F X A fld T A
81 80 rabbidv a = A w D | F w fld T × f F X a fld T a = w D | F w fld T × f F X A fld T A
82 76 81 eleq12d a = A fld T × f X a fld T a w D | F w fld T × f F X a fld T a fld T × f X A fld T A w D | F w fld T × f F X A fld T A
83 73 82 imbi12d a = A a A 0 < fld T a fld T × f X a fld T a w D | F w fld T × f F X a fld T a A A 0 < fld T A fld T × f X A fld T A w D | F w fld T × f F X A fld T A
84 83 imbi2d a = A φ a A 0 < fld T a fld T × f X a fld T a w D | F w fld T × f F X a fld T a φ A A 0 < fld T A fld T × f X A fld T A w D | F w fld T × f F X A fld T A
85 0re 0
86 85 ltnri ¬ 0 < 0
87 86 pm2.21i 0 < 0 fld T × f X 0 w D | F w fld T × f F X 0
88 87 adantl A 0 < 0 fld T × f X 0 w D | F w fld T × f F X 0
89 88 a1i φ A 0 < 0 fld T × f X 0 w D | F w fld T × f F X 0
90 impexp k A 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k k A 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k
91 simprl φ ¬ c k k c A 0 < fld T k c k c A
92 91 unssad φ ¬ c k k c A 0 < fld T k c k A
93 simpr φ ¬ c k k c A 0 < fld T k c 0 < fld T k 0 < fld T k
94 1 ad3antrrr φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k D
95 2 ad3antrrr φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k F : D
96 simplll φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k φ
97 96 3 sylan φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k a D b D a b D
98 96 4 syl φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k A Fin
99 96 5 syl φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k T : A 0 +∞
100 96 6 syl φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k X : A D
101 7 ad3antrrr φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k 0 < fld T
102 96 8 sylan φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k x D y D t 0 1 F t x + 1 t y t F x + 1 t F y
103 simpllr φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k ¬ c k
104 91 adantr φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k k c A
105 eqid fld T k = fld T k
106 eqid fld T k c = fld T k c
107 cnring fld Ring
108 ringcmn fld Ring fld CMnd
109 107 108 mp1i φ ¬ c k k c A 0 < fld T k c fld CMnd
110 4 ad2antrr φ ¬ c k k c A 0 < fld T k c A Fin
111 110 92 ssfid φ ¬ c k k c A 0 < fld T k c k Fin
112 rege0subm 0 +∞ SubMnd fld
113 112 a1i φ ¬ c k k c A 0 < fld T k c 0 +∞ SubMnd fld
114 5 ad2antrr φ ¬ c k k c A 0 < fld T k c T : A 0 +∞
115 114 92 fssresd φ ¬ c k k c A 0 < fld T k c T k : k 0 +∞
116 c0ex 0 V
117 116 a1i φ ¬ c k k c A 0 < fld T k c 0 V
118 115 111 117 fdmfifsupp φ ¬ c k k c A 0 < fld T k c finSupp 0 T k
119 21 109 111 113 115 118 gsumsubmcl φ ¬ c k k c A 0 < fld T k c fld T k 0 +∞
120 elrege0 fld T k 0 +∞ fld T k 0 fld T k
121 120 simplbi fld T k 0 +∞ fld T k
122 119 121 syl φ ¬ c k k c A 0 < fld T k c fld T k
123 122 adantr φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T k
124 simprl φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k 0 < fld T k
125 123 124 elrpd φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T k +
126 simprr φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k
127 fveq2 w = fld T × f X k fld T k F w = F fld T × f X k fld T k
128 127 breq1d w = fld T × f X k fld T k F w fld T × f F X k fld T k F fld T × f X k fld T k fld T × f F X k fld T k
129 128 elrab fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k fld T k D F fld T × f X k fld T k fld T × f F X k fld T k
130 126 129 sylib φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k fld T k D F fld T × f X k fld T k fld T × f F X k fld T k
131 130 simpld φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k fld T k D
132 130 simprd φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k F fld T × f X k fld T k fld T × f F X k fld T k
133 94 95 97 98 99 100 101 102 103 104 105 106 125 131 132 jensenlem2 φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k c fld T k c D F fld T × f X k c fld T k c fld T × f F X k c fld T k c
134 fveq2 w = fld T × f X k c fld T k c F w = F fld T × f X k c fld T k c
135 134 breq1d w = fld T × f X k c fld T k c F w fld T × f F X k c fld T k c F fld T × f X k c fld T k c fld T × f F X k c fld T k c
136 135 elrab fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c fld T × f X k c fld T k c D F fld T × f X k c fld T k c fld T × f F X k c fld T k c
137 133 136 sylibr φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
138 137 expr φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
139 93 138 embantd φ ¬ c k k c A 0 < fld T k c 0 < fld T k 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
140 cnfldbas = Base fld
141 ringmnd fld Ring fld Mnd
142 107 141 mp1i φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld Mnd
143 110 91 ssfid φ ¬ c k k c A 0 < fld T k c k c Fin
144 143 adantr φ ¬ c k k c A 0 < fld T k c 0 = fld T k k c Fin
145 ssun2 c k c
146 vsnid c c
147 145 146 sselii c k c
148 147 a1i φ ¬ c k k c A 0 < fld T k c 0 = fld T k c k c
149 remulcl x y x y
150 149 adantl φ x y x y
151 rge0ssre 0 +∞
152 fss T : A 0 +∞ 0 +∞ T : A
153 5 151 152 sylancl φ T : A
154 6 1 fssd φ X : A
155 inidm A A = A
156 150 153 154 4 4 155 off φ T × f X : A
157 ax-resscn
158 fss T × f X : A T × f X : A
159 156 157 158 sylancl φ T × f X : A
160 159 ad3antrrr φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f X : A
161 91 adantr φ ¬ c k k c A 0 < fld T k c 0 = fld T k k c A
162 160 161 fssresd φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f X k c : k c
163 5 ad3antrrr φ ¬ c k k c A 0 < fld T k c 0 = fld T k T : A 0 +∞
164 110 adantr φ ¬ c k k c A 0 < fld T k c 0 = fld T k A Fin
165 fex T : A 0 +∞ A Fin T V
166 163 164 165 syl2anc φ ¬ c k k c A 0 < fld T k c 0 = fld T k T V
167 6 ad3antrrr φ ¬ c k k c A 0 < fld T k c 0 = fld T k X : A D
168 fex X : A D A Fin X V
169 167 164 168 syl2anc φ ¬ c k k c A 0 < fld T k c 0 = fld T k X V
170 offres T V X V T × f X k c = T k c × f X k c
171 166 169 170 syl2anc φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f X k c = T k c × f X k c
172 171 oveq1d φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f X k c supp 0 = T k c × f X k c supp 0
173 151 157 sstri 0 +∞
174 fss T : A 0 +∞ 0 +∞ T : A
175 163 173 174 sylancl φ ¬ c k k c A 0 < fld T k c 0 = fld T k T : A
176 175 161 fssresd φ ¬ c k k c A 0 < fld T k c 0 = fld T k T k c : k c
177 eldifi x k c c x k c
178 177 adantl φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k c c x k c
179 178 fvresd φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k c c T k c x = T x
180 difun2 k c c = k c
181 difss k c k
182 180 181 eqsstri k c c k
183 182 sseli x k c c x k
184 simpr φ ¬ c k k c A 0 < fld T k c 0 = fld T k 0 = fld T k
185 92 adantr φ ¬ c k k c A 0 < fld T k c 0 = fld T k k A
186 163 185 feqresmpt φ ¬ c k k c A 0 < fld T k c 0 = fld T k T k = x k T x
187 186 oveq2d φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T k = fld x k T x
188 111 adantr φ ¬ c k k c A 0 < fld T k c 0 = fld T k k Fin
189 185 sselda φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k x A
190 163 ffvelrnda φ ¬ c k k c A 0 < fld T k c 0 = fld T k x A T x 0 +∞
191 189 190 syldan φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k T x 0 +∞
192 173 191 sseldi φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k T x
193 188 192 gsumfsum φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld x k T x = x k T x
194 184 187 193 3eqtrrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k T x = 0
195 elrege0 T x 0 +∞ T x 0 T x
196 191 195 sylib φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k T x 0 T x
197 196 simpld φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k T x
198 196 simprd φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k 0 T x
199 188 197 198 fsum00 φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k T x = 0 x k T x = 0
200 194 199 mpbid φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k T x = 0
201 200 r19.21bi φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k T x = 0
202 183 201 sylan2 φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k c c T x = 0
203 179 202 eqtrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k x k c c T k c x = 0
204 176 203 suppss φ ¬ c k k c A 0 < fld T k c 0 = fld T k T k c supp 0 c
205 mul02 x 0 x = 0
206 205 adantl φ ¬ c k k c A 0 < fld T k c 0 = fld T k x 0 x = 0
207 1 ad3antrrr φ ¬ c k k c A 0 < fld T k c 0 = fld T k D
208 207 157 sstrdi φ ¬ c k k c A 0 < fld T k c 0 = fld T k D
209 167 208 fssd φ ¬ c k k c A 0 < fld T k c 0 = fld T k X : A
210 209 161 fssresd φ ¬ c k k c A 0 < fld T k c 0 = fld T k X k c : k c
211 116 a1i φ ¬ c k k c A 0 < fld T k c 0 = fld T k 0 V
212 204 206 176 210 144 211 suppssof1 φ ¬ c k k c A 0 < fld T k c 0 = fld T k T k c × f X k c supp 0 c
213 172 212 eqsstrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f X k c supp 0 c
214 140 21 142 144 148 162 213 gsumpt φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T × f X k c = T × f X k c c
215 148 fvresd φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f X k c c = T × f X c
216 163 ffnd φ ¬ c k k c A 0 < fld T k c 0 = fld T k T Fn A
217 167 ffnd φ ¬ c k k c A 0 < fld T k c 0 = fld T k X Fn A
218 161 148 sseldd φ ¬ c k k c A 0 < fld T k c 0 = fld T k c A
219 fnfvof T Fn A X Fn A A Fin c A T × f X c = T c X c
220 216 217 164 218 219 syl22anc φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f X c = T c X c
221 214 215 220 3eqtrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T × f X k c = T c X c
222 140 21 142 144 148 176 204 gsumpt φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T k c = T k c c
223 148 fvresd φ ¬ c k k c A 0 < fld T k c 0 = fld T k T k c c = T c
224 222 223 eqtrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T k c = T c
225 221 224 oveq12d φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T × f X k c fld T k c = T c X c T c
226 209 218 ffvelrnd φ ¬ c k k c A 0 < fld T k c 0 = fld T k X c
227 175 218 ffvelrnd φ ¬ c k k c A 0 < fld T k c 0 = fld T k T c
228 simplrr φ ¬ c k k c A 0 < fld T k c 0 = fld T k 0 < fld T k c
229 228 224 breqtrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k 0 < T c
230 229 gt0ne0d φ ¬ c k k c A 0 < fld T k c 0 = fld T k T c 0
231 226 227 230 divcan3d φ ¬ c k k c A 0 < fld T k c 0 = fld T k T c X c T c = X c
232 225 231 eqtrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T × f X k c fld T k c = X c
233 167 218 ffvelrnd φ ¬ c k k c A 0 < fld T k c 0 = fld T k X c D
234 232 233 eqeltrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T × f X k c fld T k c D
235 2 ad3antrrr φ ¬ c k k c A 0 < fld T k c 0 = fld T k F : D
236 235 233 ffvelrnd φ ¬ c k k c A 0 < fld T k c 0 = fld T k F X c
237 236 leidd φ ¬ c k k c A 0 < fld T k c 0 = fld T k F X c F X c
238 232 fveq2d φ ¬ c k k c A 0 < fld T k c 0 = fld T k F fld T × f X k c fld T k c = F X c
239 fco F : D X : A D F X : A
240 2 6 239 syl2anc φ F X : A
241 150 153 240 4 4 155 off φ T × f F X : A
242 fss T × f F X : A T × f F X : A
243 241 157 242 sylancl φ T × f F X : A
244 243 ad3antrrr φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f F X : A
245 244 161 fssresd φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f F X k c : k c
246 240 ad3antrrr φ ¬ c k k c A 0 < fld T k c 0 = fld T k F X : A
247 fex F X : A A Fin F X V
248 246 164 247 syl2anc φ ¬ c k k c A 0 < fld T k c 0 = fld T k F X V
249 offres T V F X V T × f F X k c = T k c × f F X k c
250 166 248 249 syl2anc φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f F X k c = T k c × f F X k c
251 250 oveq1d φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f F X k c supp 0 = T k c × f F X k c supp 0
252 fss F X : A F X : A
253 246 157 252 sylancl φ ¬ c k k c A 0 < fld T k c 0 = fld T k F X : A
254 253 161 fssresd φ ¬ c k k c A 0 < fld T k c 0 = fld T k F X k c : k c
255 204 206 176 254 144 211 suppssof1 φ ¬ c k k c A 0 < fld T k c 0 = fld T k T k c × f F X k c supp 0 c
256 251 255 eqsstrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f F X k c supp 0 c
257 140 21 142 144 148 245 256 gsumpt φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T × f F X k c = T × f F X k c c
258 148 fvresd φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f F X k c c = T × f F X c
259 2 ffnd φ F Fn D
260 fnfco F Fn D X : A D F X Fn A
261 259 6 260 syl2anc φ F X Fn A
262 261 ad3antrrr φ ¬ c k k c A 0 < fld T k c 0 = fld T k F X Fn A
263 fnfvof T Fn A F X Fn A A Fin c A T × f F X c = T c F X c
264 216 262 164 218 263 syl22anc φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f F X c = T c F X c
265 fvco3 X : A D c A F X c = F X c
266 167 218 265 syl2anc φ ¬ c k k c A 0 < fld T k c 0 = fld T k F X c = F X c
267 266 oveq2d φ ¬ c k k c A 0 < fld T k c 0 = fld T k T c F X c = T c F X c
268 264 267 eqtrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k T × f F X c = T c F X c
269 257 258 268 3eqtrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T × f F X k c = T c F X c
270 269 224 oveq12d φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T × f F X k c fld T k c = T c F X c T c
271 236 recnd φ ¬ c k k c A 0 < fld T k c 0 = fld T k F X c
272 271 227 230 divcan3d φ ¬ c k k c A 0 < fld T k c 0 = fld T k T c F X c T c = F X c
273 270 272 eqtrd φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T × f F X k c fld T k c = F X c
274 237 238 273 3brtr4d φ ¬ c k k c A 0 < fld T k c 0 = fld T k F fld T × f X k c fld T k c fld T × f F X k c fld T k c
275 135 234 274 elrabd φ ¬ c k k c A 0 < fld T k c 0 = fld T k fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
276 275 a1d φ ¬ c k k c A 0 < fld T k c 0 = fld T k 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
277 120 simprbi fld T k 0 +∞ 0 fld T k
278 119 277 syl φ ¬ c k k c A 0 < fld T k c 0 fld T k
279 leloe 0 fld T k 0 fld T k 0 < fld T k 0 = fld T k
280 85 122 279 sylancr φ ¬ c k k c A 0 < fld T k c 0 fld T k 0 < fld T k 0 = fld T k
281 278 280 mpbid φ ¬ c k k c A 0 < fld T k c 0 < fld T k 0 = fld T k
282 139 276 281 mpjaodan φ ¬ c k k c A 0 < fld T k c 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
283 92 282 embantd φ ¬ c k k c A 0 < fld T k c k A 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
284 90 283 syl5bi φ ¬ c k k c A 0 < fld T k c k A 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
285 284 ex φ ¬ c k k c A 0 < fld T k c k A 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
286 285 com23 φ ¬ c k k A 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k k c A 0 < fld T k c fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
287 286 expcom ¬ c k φ k A 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k k c A 0 < fld T k c fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
288 287 adantl k Fin ¬ c k φ k A 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k k c A 0 < fld T k c fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
289 288 a2d k Fin ¬ c k φ k A 0 < fld T k fld T × f X k fld T k w D | F w fld T × f F X k fld T k φ k c A 0 < fld T k c fld T × f X k c fld T k c w D | F w fld T × f F X k c fld T k c
290 36 52 68 84 89 289 findcard2s A Fin φ A A 0 < fld T A fld T × f X A fld T A w D | F w fld T × f F X A fld T A
291 4 290 mpcom φ A A 0 < fld T A fld T × f X A fld T A w D | F w fld T × f F X A fld T A
292 15 291 mpd φ fld T × f X A fld T A w D | F w fld T × f F X A fld T A
293 156 ffnd φ T × f X Fn A
294 fnresdm T × f X Fn A T × f X A = T × f X
295 293 294 syl φ T × f X A = T × f X
296 295 oveq2d φ fld T × f X A = fld T × f X
297 296 12 oveq12d φ fld T × f X A fld T A = fld T × f X fld T
298 9 261 4 4 155 offn φ T × f F X Fn A
299 fnresdm T × f F X Fn A T × f F X A = T × f F X
300 298 299 syl φ T × f F X A = T × f F X
301 300 oveq2d φ fld T × f F X A = fld T × f F X
302 301 12 oveq12d φ fld T × f F X A fld T A = fld T × f F X fld T
303 302 breq2d φ F w fld T × f F X A fld T A F w fld T × f F X fld T
304 303 rabbidv φ w D | F w fld T × f F X A fld T A = w D | F w fld T × f F X fld T
305 292 297 304 3eltr3d φ fld T × f X fld T w D | F w fld T × f F X fld T
306 fveq2 w = fld T × f X fld T F w = F fld T × f X fld T
307 306 breq1d w = fld T × f X fld T F w fld T × f F X fld T F fld T × f X fld T fld T × f F X fld T
308 307 elrab fld T × f X fld T w D | F w fld T × f F X fld T fld T × f X fld T D F fld T × f X fld T fld T × f F X fld T
309 305 308 sylib φ fld T × f X fld T D F fld T × f X fld T fld T × f F X fld T