Metamath Proof Explorer

Theorem fsumiunle

Description: Upper bound for a sum of nonnegative terms over an indexed union. The inequality may be strict if the indexed union is non-disjoint, since in the right hand side, a summand may be counted several times. (Contributed by Thierry Arnoux, 1-Jan-2021)

Ref Expression
Hypotheses fsumiunle.1 
|- ( ph -> A e. Fin )
fsumiunle.2 
|- ( ( ph /\ x e. A ) -> B e. Fin )
fsumiunle.3 
|- ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. RR )
fsumiunle.4 
|- ( ( ( ph /\ x e. A ) /\ k e. B ) -> 0 <_ C )
Assertion fsumiunle 
|- ( ph -> sum_ k e. U_ x e. A B C <_ sum_ x e. A sum_ k e. B C )

Proof

Step Hyp Ref Expression
1 fsumiunle.1 
 |-  ( ph -> A e. Fin )
2 fsumiunle.2 
 |-  ( ( ph /\ x e. A ) -> B e. Fin )
3 fsumiunle.3 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. RR )
4 fsumiunle.4 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> 0 <_ C )
5 1 2 aciunf1 
 |-  ( ph -> E. f ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) )
6 f1f1orn 
 |-  ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) -> f : U_ x e. A B -1-1-onto-> ran f )
7 6 anim1i 
 |-  ( ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) )
8 f1f 
 |-  ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) -> f : U_ x e. A B --> U_ x e. A ( { x } X. B ) )
9 8 frnd 
 |-  ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) -> ran f C_ U_ x e. A ( { x } X. B ) )
10 9 adantr 
 |-  ( ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) -> ran f C_ U_ x e. A ( { x } X. B ) )
11 7 10 jca 
 |-  ( ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) )
12 11 eximi 
 |-  ( E. f ( f : U_ x e. A B -1-1-> U_ x e. A ( { x } X. B ) /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) -> E. f ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) )
13 5 12 syl 
 |-  ( ph -> E. f ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) )
14 csbeq1a 
 |-  ( k = y -> C = [_ y / k ]_ C )
15 nfcv 
 |-  F/_ y U_ x e. A B
16 nfcv 
 |-  F/_ k U_ x e. A B
17 nfcv 
 |-  F/_ y C
18 nfcsb1v 
 |-  F/_ k [_ y / k ]_ C
19 14 15 16 17 18 cbvsum 
 |-  sum_ k e. U_ x e. A B C = sum_ y e. U_ x e. A B [_ y / k ]_ C
20 csbeq1 
 |-  ( y = ( 2nd ` z ) -> [_ y / k ]_ C = [_ ( 2nd ` z ) / k ]_ C )
21 snfi 
 |-  { x } e. Fin
22 xpfi 
 |-  ( ( { x } e. Fin /\ B e. Fin ) -> ( { x } X. B ) e. Fin )
23 21 2 22 sylancr 
 |-  ( ( ph /\ x e. A ) -> ( { x } X. B ) e. Fin )
24 23 ralrimiva 
 |-  ( ph -> A. x e. A ( { x } X. B ) e. Fin )
25 iunfi 
 |-  ( ( A e. Fin /\ A. x e. A ( { x } X. B ) e. Fin ) -> U_ x e. A ( { x } X. B ) e. Fin )
26 1 24 25 syl2anc 
 |-  ( ph -> U_ x e. A ( { x } X. B ) e. Fin )
27 26 adantr 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> U_ x e. A ( { x } X. B ) e. Fin )
28 simprr 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> ran f C_ U_ x e. A ( { x } X. B ) )
29 27 28 ssfid 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> ran f e. Fin )
30 simprl 
 |-  ( ( ph /\ ( f : U_ x e. A B -1-1-onto-> ran f /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> f : U_ x e. A B -1-1-onto-> ran f )
31 f1ocnv 
 |-  ( f : U_ x e. A B -1-1-onto-> ran f -> `' f : ran f -1-1-onto-> U_ x e. A B )
32 30 31 syl 
 |-  ( ( ph /\ ( f : U_ x e. A B -1-1-onto-> ran f /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> `' f : ran f -1-1-onto-> U_ x e. A B )
33 32 adantrlr 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> `' f : ran f -1-1-onto-> U_ x e. A B )
34 nfv 
 |-  F/ x ph
35 nfcv 
 |-  F/_ x f
36 nfiu1 
 |-  F/_ x U_ x e. A B
37 35 nfrn 
 |-  F/_ x ran f
38 35 36 37 nff1o 
 |-  F/ x f : U_ x e. A B -1-1-onto-> ran f
39 nfv 
 |-  F/ x ( 2nd ` ( f ` l ) ) = l
40 36 39 nfralw 
 |-  F/ x A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l
41 38 40 nfan 
 |-  F/ x ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l )
42 nfcv 
 |-  F/_ x ran f
43 nfiu1 
 |-  F/_ x U_ x e. A ( { x } X. B )
44 42 43 nfss 
 |-  F/ x ran f C_ U_ x e. A ( { x } X. B )
45 41 44 nfan 
 |-  F/ x ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) )
46 34 45 nfan 
 |-  F/ x ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) )
47 nfv 
 |-  F/ x z e. ran f
48 46 47 nfan 
 |-  F/ x ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f )
49 simpr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( f ` k ) = z )
50 49 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` ( f ` k ) ) = ( 2nd ` z ) )
51 simplr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> k e. U_ x e. A B )
52 simp-4r 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) )
53 52 simpld 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) )
54 53 simprd 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l )
55 54 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l )
56 2fveq3 
 |-  ( l = k -> ( 2nd ` ( f ` l ) ) = ( 2nd ` ( f ` k ) ) )
57 id 
 |-  ( l = k -> l = k )
58 56 57 eqeq12d 
 |-  ( l = k -> ( ( 2nd ` ( f ` l ) ) = l <-> ( 2nd ` ( f ` k ) ) = k ) )
59 58 rspcva 
 |-  ( ( k e. U_ x e. A B /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) -> ( 2nd ` ( f ` k ) ) = k )
60 51 55 59 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` ( f ` k ) ) = k )
61 50 60 eqtr3d 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( 2nd ` z ) = k )
62 53 simpld 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> f : U_ x e. A B -1-1-onto-> ran f )
63 62 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> f : U_ x e. A B -1-1-onto-> ran f )
64 f1ocnvfv1 
 |-  ( ( f : U_ x e. A B -1-1-onto-> ran f /\ k e. U_ x e. A B ) -> ( `' f ` ( f ` k ) ) = k )
65 63 51 64 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` ( f ` k ) ) = k )
66 49 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` ( f ` k ) ) = ( `' f ` z ) )
67 61 65 66 3eqtr2rd 
 |-  ( ( ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) /\ k e. U_ x e. A B ) /\ ( f ` k ) = z ) -> ( `' f ` z ) = ( 2nd ` z ) )
68 f1ofn 
 |-  ( f : U_ x e. A B -1-1-onto-> ran f -> f Fn U_ x e. A B )
69 62 68 syl 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> f Fn U_ x e. A B )
70 simpllr 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> z e. ran f )
71 fvelrnb 
 |-  ( f Fn U_ x e. A B -> ( z e. ran f <-> E. k e. U_ x e. A B ( f ` k ) = z ) )
72 71 biimpa 
 |-  ( ( f Fn U_ x e. A B /\ z e. ran f ) -> E. k e. U_ x e. A B ( f ` k ) = z )
73 69 70 72 syl2anc 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> E. k e. U_ x e. A B ( f ` k ) = z )
74 67 73 r19.29a 
 |-  ( ( ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> ( `' f ` z ) = ( 2nd ` z ) )
75 28 sselda 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) -> z e. U_ x e. A ( { x } X. B ) )
76 eliun 
 |-  ( z e. U_ x e. A ( { x } X. B ) <-> E. x e. A z e. ( { x } X. B ) )
77 75 76 sylib 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) -> E. x e. A z e. ( { x } X. B ) )
78 48 74 77 r19.29af 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. ran f ) -> ( `' f ` z ) = ( 2nd ` z ) )
79 nfv 
 |-  F/ k ( ph /\ y e. U_ x e. A B )
80 nfcv 
 |-  F/_ k CC
81 18 80 nfel 
 |-  F/ k [_ y / k ]_ C e. CC
82 79 81 nfim 
 |-  F/ k ( ( ph /\ y e. U_ x e. A B ) -> [_ y / k ]_ C e. CC )
83 eleq1w 
 |-  ( k = y -> ( k e. U_ x e. A B <-> y e. U_ x e. A B ) )
84 83 anbi2d 
 |-  ( k = y -> ( ( ph /\ k e. U_ x e. A B ) <-> ( ph /\ y e. U_ x e. A B ) ) )
85 14 eleq1d 
 |-  ( k = y -> ( C e. CC <-> [_ y / k ]_ C e. CC ) )
86 84 85 imbi12d 
 |-  ( k = y -> ( ( ( ph /\ k e. U_ x e. A B ) -> C e. CC ) <-> ( ( ph /\ y e. U_ x e. A B ) -> [_ y / k ]_ C e. CC ) ) )
87 nfcv 
 |-  F/_ x k
88 87 36 nfel 
 |-  F/ x k e. U_ x e. A B
89 34 88 nfan 
 |-  F/ x ( ph /\ k e. U_ x e. A B )
90 3 adantllr 
 |-  ( ( ( ( ph /\ k e. U_ x e. A B ) /\ x e. A ) /\ k e. B ) -> C e. RR )
91 90 recnd 
 |-  ( ( ( ( ph /\ k e. U_ x e. A B ) /\ x e. A ) /\ k e. B ) -> C e. CC )
92 eliun 
 |-  ( k e. U_ x e. A B <-> E. x e. A k e. B )
93 92 biimpi 
 |-  ( k e. U_ x e. A B -> E. x e. A k e. B )
94 93 adantl 
 |-  ( ( ph /\ k e. U_ x e. A B ) -> E. x e. A k e. B )
95 89 91 94 r19.29af 
 |-  ( ( ph /\ k e. U_ x e. A B ) -> C e. CC )
96 82 86 95 chvarfv 
 |-  ( ( ph /\ y e. U_ x e. A B ) -> [_ y / k ]_ C e. CC )
97 96 adantlr 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ y e. U_ x e. A B ) -> [_ y / k ]_ C e. CC )
98 20 29 33 78 97 fsumf1o 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ y e. U_ x e. A B [_ y / k ]_ C = sum_ z e. ran f [_ ( 2nd ` z ) / k ]_ C )
99 19 98 syl5eq 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ k e. U_ x e. A B C = sum_ z e. ran f [_ ( 2nd ` z ) / k ]_ C )
100 99 eqcomd 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ z e. ran f [_ ( 2nd ` z ) / k ]_ C = sum_ k e. U_ x e. A B C )
101 nfcv 
 |-  F/_ x z
102 101 43 nfel 
 |-  F/ x z e. U_ x e. A ( { x } X. B )
103 34 102 nfan 
 |-  F/ x ( ph /\ z e. U_ x e. A ( { x } X. B ) )
104 xp2nd 
 |-  ( z e. ( { x } X. B ) -> ( 2nd ` z ) e. B )
105 104 adantl 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> ( 2nd ` z ) e. B )
106 3 ralrimiva 
 |-  ( ( ph /\ x e. A ) -> A. k e. B C e. RR )
107 106 adantlr 
 |-  ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) -> A. k e. B C e. RR )
108 107 adantr 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> A. k e. B C e. RR )
109 nfcsb1v 
 |-  F/_ k [_ ( 2nd ` z ) / k ]_ C
110 109 nfel1 
 |-  F/ k [_ ( 2nd ` z ) / k ]_ C e. RR
111 csbeq1a 
 |-  ( k = ( 2nd ` z ) -> C = [_ ( 2nd ` z ) / k ]_ C )
112 111 eleq1d 
 |-  ( k = ( 2nd ` z ) -> ( C e. RR <-> [_ ( 2nd ` z ) / k ]_ C e. RR ) )
113 110 112 rspc 
 |-  ( ( 2nd ` z ) e. B -> ( A. k e. B C e. RR -> [_ ( 2nd ` z ) / k ]_ C e. RR ) )
114 113 imp 
 |-  ( ( ( 2nd ` z ) e. B /\ A. k e. B C e. RR ) -> [_ ( 2nd ` z ) / k ]_ C e. RR )
115 105 108 114 syl2anc 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. RR )
116 76 biimpi 
 |-  ( z e. U_ x e. A ( { x } X. B ) -> E. x e. A z e. ( { x } X. B ) )
117 116 adantl 
 |-  ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) -> E. x e. A z e. ( { x } X. B ) )
118 103 115 117 r19.29af 
 |-  ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. RR )
119 118 adantlr 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. U_ x e. A ( { x } X. B ) ) -> [_ ( 2nd ` z ) / k ]_ C e. RR )
120 xp1st 
 |-  ( z e. ( { x } X. B ) -> ( 1st ` z ) e. { x } )
121 elsni 
 |-  ( ( 1st ` z ) e. { x } -> ( 1st ` z ) = x )
122 120 121 syl 
 |-  ( z e. ( { x } X. B ) -> ( 1st ` z ) = x )
123 122 104 jca 
 |-  ( z e. ( { x } X. B ) -> ( ( 1st ` z ) = x /\ ( 2nd ` z ) e. B ) )
124 simplll 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ ( ( 1st ` z ) = x /\ ( 2nd ` z ) e. B ) ) -> ph )
125 simplr 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ ( ( 1st ` z ) = x /\ ( 2nd ` z ) e. B ) ) -> x e. A )
126 4 ralrimiva 
 |-  ( ( ph /\ x e. A ) -> A. k e. B 0 <_ C )
127 124 125 126 syl2anc 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ ( ( 1st ` z ) = x /\ ( 2nd ` z ) e. B ) ) -> A. k e. B 0 <_ C )
128 123 127 sylan2 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> A. k e. B 0 <_ C )
129 nfcv 
 |-  F/_ k 0
130 nfcv 
 |-  F/_ k <_
131 129 130 109 nfbr 
 |-  F/ k 0 <_ [_ ( 2nd ` z ) / k ]_ C
132 111 breq2d 
 |-  ( k = ( 2nd ` z ) -> ( 0 <_ C <-> 0 <_ [_ ( 2nd ` z ) / k ]_ C ) )
133 131 132 rspc 
 |-  ( ( 2nd ` z ) e. B -> ( A. k e. B 0 <_ C -> 0 <_ [_ ( 2nd ` z ) / k ]_ C ) )
134 133 imp 
 |-  ( ( ( 2nd ` z ) e. B /\ A. k e. B 0 <_ C ) -> 0 <_ [_ ( 2nd ` z ) / k ]_ C )
135 105 128 134 syl2anc 
 |-  ( ( ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) /\ x e. A ) /\ z e. ( { x } X. B ) ) -> 0 <_ [_ ( 2nd ` z ) / k ]_ C )
136 103 135 117 r19.29af 
 |-  ( ( ph /\ z e. U_ x e. A ( { x } X. B ) ) -> 0 <_ [_ ( 2nd ` z ) / k ]_ C )
137 136 adantlr 
 |-  ( ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) /\ z e. U_ x e. A ( { x } X. B ) ) -> 0 <_ [_ ( 2nd ` z ) / k ]_ C )
138 27 119 137 28 fsumless 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ z e. ran f [_ ( 2nd ` z ) / k ]_ C <_ sum_ z e. U_ x e. A ( { x } X. B ) [_ ( 2nd ` z ) / k ]_ C )
139 100 138 eqbrtrrd 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ k e. U_ x e. A B C <_ sum_ z e. U_ x e. A ( { x } X. B ) [_ ( 2nd ` z ) / k ]_ C )
140 nfcv 
 |-  F/_ y B
141 nfcv 
 |-  F/_ k B
142 14 140 141 17 18 cbvsum 
 |-  sum_ k e. B C = sum_ y e. B [_ y / k ]_ C
143 142 a1i 
 |-  ( ph -> sum_ k e. B C = sum_ y e. B [_ y / k ]_ C )
144 143 sumeq2sdv 
 |-  ( ph -> sum_ x e. A sum_ k e. B C = sum_ x e. A sum_ y e. B [_ y / k ]_ C )
145 vex 
 |-  x e. _V
146 vex 
 |-  y e. _V
147 145 146 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
148 147 eqcomd 
 |-  ( z = <. x , y >. -> y = ( 2nd ` z ) )
149 148 csbeq1d 
 |-  ( z = <. x , y >. -> [_ y / k ]_ C = [_ ( 2nd ` z ) / k ]_ C )
150 149 eqcomd 
 |-  ( z = <. x , y >. -> [_ ( 2nd ` z ) / k ]_ C = [_ y / k ]_ C )
151 nfv 
 |-  F/ k ( ( ph /\ x e. A ) /\ y e. B )
152 18 nfel1 
 |-  F/ k [_ y / k ]_ C e. CC
153 151 152 nfim 
 |-  F/ k ( ( ( ph /\ x e. A ) /\ y e. B ) -> [_ y / k ]_ C e. CC )
154 eleq1w 
 |-  ( k = y -> ( k e. B <-> y e. B ) )
155 154 anbi2d 
 |-  ( k = y -> ( ( ( ph /\ x e. A ) /\ k e. B ) <-> ( ( ph /\ x e. A ) /\ y e. B ) ) )
156 155 85 imbi12d 
 |-  ( k = y -> ( ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. CC ) <-> ( ( ( ph /\ x e. A ) /\ y e. B ) -> [_ y / k ]_ C e. CC ) ) )
157 3 recnd 
 |-  ( ( ( ph /\ x e. A ) /\ k e. B ) -> C e. CC )
158 153 156 157 chvarfv 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> [_ y / k ]_ C e. CC )
159 158 anasss 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> [_ y / k ]_ C e. CC )
160 150 1 2 159 fsum2d 
 |-  ( ph -> sum_ x e. A sum_ y e. B [_ y / k ]_ C = sum_ z e. U_ x e. A ( { x } X. B ) [_ ( 2nd ` z ) / k ]_ C )
161 144 160 eqtrd 
 |-  ( ph -> sum_ x e. A sum_ k e. B C = sum_ z e. U_ x e. A ( { x } X. B ) [_ ( 2nd ` z ) / k ]_ C )
162 161 adantr 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ x e. A sum_ k e. B C = sum_ z e. U_ x e. A ( { x } X. B ) [_ ( 2nd ` z ) / k ]_ C )
163 139 162 breqtrrd 
 |-  ( ( ph /\ ( ( f : U_ x e. A B -1-1-onto-> ran f /\ A. l e. U_ x e. A B ( 2nd ` ( f ` l ) ) = l ) /\ ran f C_ U_ x e. A ( { x } X. B ) ) ) -> sum_ k e. U_ x e. A B C <_ sum_ x e. A sum_ k e. B C )
164 13 163 exlimddv 
 |-  ( ph -> sum_ k e. U_ x e. A B C <_ sum_ x e. A sum_ k e. B C )