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