Metamath Proof Explorer

Theorem carsgclctunlem2

Description: Lemma for carsgclctun . (Contributed by Thierry Arnoux, 25-May-2020)

Ref Expression
Hypotheses carsgval.1 
|- ( ph -> O e. V )
carsgval.2 
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
carsgsiga.1 
|- ( ph -> ( M ` (/) ) = 0 )
carsgsiga.2 
|- ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
carsgsiga.3 
|- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
carsgclctunlem2.1 
|- ( ph -> Disj_ k e. NN A )
carsgclctunlem2.2 
|- ( ( ph /\ k e. NN ) -> A e. ( toCaraSiga ` M ) )
carsgclctunlem2.3 
|- ( ph -> E e. ~P O )
carsgclctunlem2.4 
|- ( ph -> ( M ` E ) =/= +oo )
Assertion carsgclctunlem2 
|- ( ph -> ( ( M ` ( E i^i U_ k e. NN A ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) <_ ( M ` E ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 
 |-  ( ph -> O e. V )
2 carsgval.2 
 |-  ( ph -> M : ~P O --> ( 0 [,] +oo ) )
3 carsgsiga.1 
 |-  ( ph -> ( M ` (/) ) = 0 )
4 carsgsiga.2 
 |-  ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
5 carsgsiga.3 
 |-  ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
6 carsgclctunlem2.1 
 |-  ( ph -> Disj_ k e. NN A )
7 carsgclctunlem2.2 
 |-  ( ( ph /\ k e. NN ) -> A e. ( toCaraSiga ` M ) )
8 carsgclctunlem2.3 
 |-  ( ph -> E e. ~P O )
9 carsgclctunlem2.4 
 |-  ( ph -> ( M ` E ) =/= +oo )
10 iunin2 
 |-  U_ k e. NN ( E i^i A ) = ( E i^i U_ k e. NN A )
11 10 fveq2i 
 |-  ( M ` U_ k e. NN ( E i^i A ) ) = ( M ` ( E i^i U_ k e. NN A ) )
12 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
13 nnex 
 |-  NN e. _V
14 13 a1i 
 |-  ( ph -> NN e. _V )
15 8 adantr 
 |-  ( ( ph /\ k e. NN ) -> E e. ~P O )
16 15 elpwincl1 
 |-  ( ( ph /\ k e. NN ) -> ( E i^i A ) e. ~P O )
17 14 16 elpwiuncl 
 |-  ( ph -> U_ k e. NN ( E i^i A ) e. ~P O )
18 2 17 ffvelrnd 
 |-  ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) e. ( 0 [,] +oo ) )
19 12 18 sseldi 
 |-  ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) e. RR* )
20 11 19 eqeltrrid 
 |-  ( ph -> ( M ` ( E i^i U_ k e. NN A ) ) e. RR* )
21 2 8 ffvelrnd 
 |-  ( ph -> ( M ` E ) e. ( 0 [,] +oo ) )
22 12 21 sseldi 
 |-  ( ph -> ( M ` E ) e. RR* )
23 8 elpwdifcl 
 |-  ( ph -> ( E \ U_ k e. NN A ) e. ~P O )
24 2 23 ffvelrnd 
 |-  ( ph -> ( M ` ( E \ U_ k e. NN A ) ) e. ( 0 [,] +oo ) )
25 12 24 sseldi 
 |-  ( ph -> ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
26 25 xnegcld 
 |-  ( ph -> -e ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
27 22 26 xaddcld 
 |-  ( ph -> ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) e. RR* )
28 2 adantr 
 |-  ( ( ph /\ k e. NN ) -> M : ~P O --> ( 0 [,] +oo ) )
29 28 16 ffvelrnd 
 |-  ( ( ph /\ k e. NN ) -> ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
30 29 ralrimiva 
 |-  ( ph -> A. k e. NN ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
31 nfcv 
 |-  F/_ k NN
32 31 esumcl 
 |-  ( ( NN e. _V /\ A. k e. NN ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) ) -> sum* k e. NN ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
33 14 30 32 syl2anc 
 |-  ( ph -> sum* k e. NN ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
34 12 33 sseldi 
 |-  ( ph -> sum* k e. NN ( M ` ( E i^i A ) ) e. RR* )
35 16 ralrimiva 
 |-  ( ph -> A. k e. NN ( E i^i A ) e. ~P O )
36 dfiun3g 
 |-  ( A. k e. NN ( E i^i A ) e. ~P O -> U_ k e. NN ( E i^i A ) = U. ran ( k e. NN |-> ( E i^i A ) ) )
37 35 36 syl 
 |-  ( ph -> U_ k e. NN ( E i^i A ) = U. ran ( k e. NN |-> ( E i^i A ) ) )
38 37 fveq2d 
 |-  ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) = ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) )
39 nnct 
 |-  NN ~<_ _om
40 mptct 
 |-  ( NN ~<_ _om -> ( k e. NN |-> ( E i^i A ) ) ~<_ _om )
41 rnct 
 |-  ( ( k e. NN |-> ( E i^i A ) ) ~<_ _om -> ran ( k e. NN |-> ( E i^i A ) ) ~<_ _om )
42 39 40 41 mp2b 
 |-  ran ( k e. NN |-> ( E i^i A ) ) ~<_ _om
43 42 a1i 
 |-  ( ph -> ran ( k e. NN |-> ( E i^i A ) ) ~<_ _om )
44 eqid 
 |-  ( k e. NN |-> ( E i^i A ) ) = ( k e. NN |-> ( E i^i A ) )
45 44 rnmptss 
 |-  ( A. k e. NN ( E i^i A ) e. ~P O -> ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O )
46 35 45 syl 
 |-  ( ph -> ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O )
47 mptexg 
 |-  ( NN e. _V -> ( k e. NN |-> ( E i^i A ) ) e. _V )
48 rnexg 
 |-  ( ( k e. NN |-> ( E i^i A ) ) e. _V -> ran ( k e. NN |-> ( E i^i A ) ) e. _V )
49 13 47 48 mp2b 
 |-  ran ( k e. NN |-> ( E i^i A ) ) e. _V
50 breq1 
 |-  ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( x ~<_ _om <-> ran ( k e. NN |-> ( E i^i A ) ) ~<_ _om ) )
51 sseq1 
 |-  ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( x C_ ~P O <-> ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O ) )
52 50 51 3anbi23d 
 |-  ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) <-> ( ph /\ ran ( k e. NN |-> ( E i^i A ) ) ~<_ _om /\ ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O ) ) )
53 unieq 
 |-  ( x = ran ( k e. NN |-> ( E i^i A ) ) -> U. x = U. ran ( k e. NN |-> ( E i^i A ) ) )
54 53 fveq2d 
 |-  ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( M ` U. x ) = ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) )
55 esumeq1 
 |-  ( x = ran ( k e. NN |-> ( E i^i A ) ) -> sum* y e. x ( M ` y ) = sum* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) )
56 54 55 breq12d 
 |-  ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( ( M ` U. x ) <_ sum* y e. x ( M ` y ) <-> ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) <_ sum* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) ) )
57 52 56 imbi12d 
 |-  ( x = ran ( k e. NN |-> ( E i^i A ) ) -> ( ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) ) <-> ( ( ph /\ ran ( k e. NN |-> ( E i^i A ) ) ~<_ _om /\ ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O ) -> ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) <_ sum* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) ) ) )
58 57 4 vtoclg 
 |-  ( ran ( k e. NN |-> ( E i^i A ) ) e. _V -> ( ( ph /\ ran ( k e. NN |-> ( E i^i A ) ) ~<_ _om /\ ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O ) -> ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) <_ sum* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) ) )
59 49 58 ax-mp 
 |-  ( ( ph /\ ran ( k e. NN |-> ( E i^i A ) ) ~<_ _om /\ ran ( k e. NN |-> ( E i^i A ) ) C_ ~P O ) -> ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) <_ sum* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) )
60 43 46 59 mpd3an23 
 |-  ( ph -> ( M ` U. ran ( k e. NN |-> ( E i^i A ) ) ) <_ sum* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) )
61 38 60 eqbrtrd 
 |-  ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) <_ sum* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) )
62 fveq2 
 |-  ( y = ( E i^i A ) -> ( M ` y ) = ( M ` ( E i^i A ) ) )
63 simpr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( E i^i A ) = (/) ) -> ( E i^i A ) = (/) )
64 63 fveq2d 
 |-  ( ( ( ph /\ k e. NN ) /\ ( E i^i A ) = (/) ) -> ( M ` ( E i^i A ) ) = ( M ` (/) ) )
65 3 ad2antrr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( E i^i A ) = (/) ) -> ( M ` (/) ) = 0 )
66 64 65 eqtrd 
 |-  ( ( ( ph /\ k e. NN ) /\ ( E i^i A ) = (/) ) -> ( M ` ( E i^i A ) ) = 0 )
67 disjin 
 |-  ( Disj_ k e. NN A -> Disj_ k e. NN ( A i^i E ) )
68 6 67 syl 
 |-  ( ph -> Disj_ k e. NN ( A i^i E ) )
69 incom 
 |-  ( A i^i E ) = ( E i^i A )
70 69 rgenw 
 |-  A. k e. NN ( A i^i E ) = ( E i^i A )
71 disjeq2 
 |-  ( A. k e. NN ( A i^i E ) = ( E i^i A ) -> ( Disj_ k e. NN ( A i^i E ) <-> Disj_ k e. NN ( E i^i A ) ) )
72 70 71 ax-mp 
 |-  ( Disj_ k e. NN ( A i^i E ) <-> Disj_ k e. NN ( E i^i A ) )
73 68 72 sylib 
 |-  ( ph -> Disj_ k e. NN ( E i^i A ) )
74 62 14 29 16 66 73 esumrnmpt2 
 |-  ( ph -> sum* y e. ran ( k e. NN |-> ( E i^i A ) ) ( M ` y ) = sum* k e. NN ( M ` ( E i^i A ) ) )
75 61 74 breqtrd 
 |-  ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) <_ sum* k e. NN ( M ` ( E i^i A ) ) )
76 difssd 
 |-  ( ph -> ( E \ U_ k e. NN A ) C_ E )
77 1 2 76 8 5 carsgmon 
 |-  ( ph -> ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` E ) )
78 21 24 77 xrge0subcld 
 |-  ( ph -> ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) e. ( 0 [,] +oo ) )
79 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> M : ~P O --> ( 0 [,] +oo ) )
80 8 adantr 
 |-  ( ( ph /\ n e. NN ) -> E e. ~P O )
81 80 elpwincl1 
 |-  ( ( ph /\ n e. NN ) -> ( E i^i U_ k e. ( 1 ... n ) A ) e. ~P O )
82 79 81 ffvelrnd 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. ( 0 [,] +oo ) )
83 12 82 sseldi 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. RR* )
84 xrge0neqmnf 
 |-  ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. ( 0 [,] +oo ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) =/= -oo )
85 82 84 syl 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) =/= -oo )
86 80 elpwdifcl 
 |-  ( ( ph /\ n e. NN ) -> ( E \ U_ k e. ( 1 ... n ) A ) e. ~P O )
87 79 86 ffvelrnd 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. ( 0 [,] +oo ) )
88 12 87 sseldi 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* )
89 xrge0neqmnf 
 |-  ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. ( 0 [,] +oo ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo )
90 87 89 syl 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo )
91 88 xnegcld 
 |-  ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* )
92 xnegneg 
 |-  ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
93 88 92 syl 
 |-  ( ( ph /\ n e. NN ) -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
94 93 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
95 xnegeq 
 |-  ( -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -e -oo )
96 95 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -e -oo )
97 xnegmnf 
 |-  -e -oo = +oo
98 96 97 eqtrdi 
 |-  ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> -e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = +oo )
99 94 98 eqtr3d 
 |-  ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = +oo )
100 99 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e +oo ) )
101 simpll 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ph )
102 fz1ssnn 
 |-  ( 1 ... n ) C_ NN
103 102 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) C_ NN )
104 103 sselda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
105 101 104 7 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. ( toCaraSiga ` M ) )
106 105 ralrimiva 
 |-  ( ( ph /\ n e. NN ) -> A. k e. ( 1 ... n ) A e. ( toCaraSiga ` M ) )
107 dfiun3g 
 |-  ( A. k e. ( 1 ... n ) A e. ( toCaraSiga ` M ) -> U_ k e. ( 1 ... n ) A = U. ran ( k e. ( 1 ... n ) |-> A ) )
108 106 107 syl 
 |-  ( ( ph /\ n e. NN ) -> U_ k e. ( 1 ... n ) A = U. ran ( k e. ( 1 ... n ) |-> A ) )
109 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> O e. V )
110 3 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( M ` (/) ) = 0 )
111 4 3adant1r 
 |-  ( ( ( ph /\ n e. NN ) /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
112 fzfi 
 |-  ( 1 ... n ) e. Fin
113 mptfi 
 |-  ( ( 1 ... n ) e. Fin -> ( k e. ( 1 ... n ) |-> A ) e. Fin )
114 rnfi 
 |-  ( ( k e. ( 1 ... n ) |-> A ) e. Fin -> ran ( k e. ( 1 ... n ) |-> A ) e. Fin )
115 112 113 114 mp2b 
 |-  ran ( k e. ( 1 ... n ) |-> A ) e. Fin
116 115 a1i 
 |-  ( ( ph /\ n e. NN ) -> ran ( k e. ( 1 ... n ) |-> A ) e. Fin )
117 eqid 
 |-  ( k e. ( 1 ... n ) |-> A ) = ( k e. ( 1 ... n ) |-> A )
118 117 rnmptss 
 |-  ( A. k e. ( 1 ... n ) A e. ( toCaraSiga ` M ) -> ran ( k e. ( 1 ... n ) |-> A ) C_ ( toCaraSiga ` M ) )
119 106 118 syl 
 |-  ( ( ph /\ n e. NN ) -> ran ( k e. ( 1 ... n ) |-> A ) C_ ( toCaraSiga ` M ) )
120 109 79 110 111 116 119 fiunelcarsg 
 |-  ( ( ph /\ n e. NN ) -> U. ran ( k e. ( 1 ... n ) |-> A ) e. ( toCaraSiga ` M ) )
121 108 120 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> U_ k e. ( 1 ... n ) A e. ( toCaraSiga ` M ) )
122 109 79 elcarsg 
 |-  ( ( ph /\ n e. NN ) -> ( U_ k e. ( 1 ... n ) A e. ( toCaraSiga ` M ) <-> ( U_ k e. ( 1 ... n ) A C_ O /\ A. e e. ~P O ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` e ) ) ) )
123 121 122 mpbid 
 |-  ( ( ph /\ n e. NN ) -> ( U_ k e. ( 1 ... n ) A C_ O /\ A. e e. ~P O ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` e ) ) )
124 123 simprd 
 |-  ( ( ph /\ n e. NN ) -> A. e e. ~P O ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` e ) )
125 ineq1 
 |-  ( e = E -> ( e i^i U_ k e. ( 1 ... n ) A ) = ( E i^i U_ k e. ( 1 ... n ) A ) )
126 125 fveq2d 
 |-  ( e = E -> ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) )
127 difeq1 
 |-  ( e = E -> ( e \ U_ k e. ( 1 ... n ) A ) = ( E \ U_ k e. ( 1 ... n ) A ) )
128 127 fveq2d 
 |-  ( e = E -> ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
129 126 128 oveq12d 
 |-  ( e = E -> ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) )
130 fveq2 
 |-  ( e = E -> ( M ` e ) = ( M ` E ) )
131 129 130 eqeq12d 
 |-  ( e = E -> ( ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` e ) <-> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` E ) ) )
132 131 rspcv 
 |-  ( E e. ~P O -> ( A. e e. ~P O ( ( M ` ( e i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( e \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` e ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` E ) ) )
133 80 124 132 sylc 
 |-  ( ( ph /\ n e. NN ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` E ) )
134 133 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` E ) )
135 xaddpnf1 
 |-  ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. RR* /\ ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) =/= -oo ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e +oo ) = +oo )
136 83 85 135 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e +oo ) = +oo )
137 136 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e +oo ) = +oo )
138 100 134 137 3eqtr3d 
 |-  ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( M ` E ) = +oo )
139 9 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> ( M ` E ) =/= +oo )
140 139 neneqd 
 |-  ( ( ( ph /\ n e. NN ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo ) -> -. ( M ` E ) = +oo )
141 138 140 pm2.65da 
 |-  ( ( ph /\ n e. NN ) -> -. -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) = -oo )
142 141 neqned 
 |-  ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo )
143 xaddass 
 |-  ( ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. RR* /\ ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) =/= -oo ) /\ ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* /\ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo ) /\ ( -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) =/= -oo ) ) -> ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) ) )
144 83 85 88 90 91 142 143 syl222anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) ) )
145 xnegid 
 |-  ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* -> ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = 0 )
146 88 145 syl 
 |-  ( ( ph /\ n e. NN ) -> ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = 0 )
147 146 oveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) ) = ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e 0 ) )
148 xaddid1 
 |-  ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) e. RR* -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e 0 ) = ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) )
149 83 148 syl 
 |-  ( ( ph /\ n e. NN ) -> ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e 0 ) = ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) )
150 144 147 149 3eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) )
151 133 oveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) +e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) = ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) )
152 108 ineq2d 
 |-  ( ( ph /\ n e. NN ) -> ( E i^i U_ k e. ( 1 ... n ) A ) = ( E i^i U. ran ( k e. ( 1 ... n ) |-> A ) ) )
153 152 fveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) = ( M ` ( E i^i U. ran ( k e. ( 1 ... n ) |-> A ) ) ) )
154 mptss 
 |-  ( ( 1 ... n ) C_ NN -> ( k e. ( 1 ... n ) |-> A ) C_ ( k e. NN |-> A ) )
155 rnss 
 |-  ( ( k e. ( 1 ... n ) |-> A ) C_ ( k e. NN |-> A ) -> ran ( k e. ( 1 ... n ) |-> A ) C_ ran ( k e. NN |-> A ) )
156 102 154 155 mp2b 
 |-  ran ( k e. ( 1 ... n ) |-> A ) C_ ran ( k e. NN |-> A )
157 156 a1i 
 |-  ( ( ph /\ n e. NN ) -> ran ( k e. ( 1 ... n ) |-> A ) C_ ran ( k e. NN |-> A ) )
158 disjrnmpt 
 |-  ( Disj_ k e. NN A -> Disj_ y e. ran ( k e. NN |-> A ) y )
159 6 158 syl 
 |-  ( ph -> Disj_ y e. ran ( k e. NN |-> A ) y )
160 159 adantr 
 |-  ( ( ph /\ n e. NN ) -> Disj_ y e. ran ( k e. NN |-> A ) y )
161 disjss1 
 |-  ( ran ( k e. ( 1 ... n ) |-> A ) C_ ran ( k e. NN |-> A ) -> ( Disj_ y e. ran ( k e. NN |-> A ) y -> Disj_ y e. ran ( k e. ( 1 ... n ) |-> A ) y ) )
162 157 160 161 sylc 
 |-  ( ( ph /\ n e. NN ) -> Disj_ y e. ran ( k e. ( 1 ... n ) |-> A ) y )
163 109 79 110 111 116 119 162 80 carsgclctunlem1 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U. ran ( k e. ( 1 ... n ) |-> A ) ) ) = sum* y e. ran ( k e. ( 1 ... n ) |-> A ) ( M ` ( E i^i y ) ) )
164 ineq2 
 |-  ( y = A -> ( E i^i y ) = ( E i^i A ) )
165 164 fveq2d 
 |-  ( y = A -> ( M ` ( E i^i y ) ) = ( M ` ( E i^i A ) ) )
166 112 elexi 
 |-  ( 1 ... n ) e. _V
167 166 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) e. _V )
168 101 104 29 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( M ` ( E i^i A ) ) e. ( 0 [,] +oo ) )
169 inss2 
 |-  ( E i^i A ) C_ A
170 sseq2 
 |-  ( A = (/) -> ( ( E i^i A ) C_ A <-> ( E i^i A ) C_ (/) ) )
171 169 170 mpbii 
 |-  ( A = (/) -> ( E i^i A ) C_ (/) )
172 ss0 
 |-  ( ( E i^i A ) C_ (/) -> ( E i^i A ) = (/) )
173 171 172 syl 
 |-  ( A = (/) -> ( E i^i A ) = (/) )
174 173 adantl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( E i^i A ) = (/) )
175 174 fveq2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( M ` ( E i^i A ) ) = ( M ` (/) ) )
176 110 ad2antrr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( M ` (/) ) = 0 )
177 175 176 eqtrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ A = (/) ) -> ( M ` ( E i^i A ) ) = 0 )
178 6 adantr 
 |-  ( ( ph /\ n e. NN ) -> Disj_ k e. NN A )
179 disjss1 
 |-  ( ( 1 ... n ) C_ NN -> ( Disj_ k e. NN A -> Disj_ k e. ( 1 ... n ) A ) )
180 103 178 179 sylc 
 |-  ( ( ph /\ n e. NN ) -> Disj_ k e. ( 1 ... n ) A )
181 165 167 168 105 177 180 esumrnmpt2 
 |-  ( ( ph /\ n e. NN ) -> sum* y e. ran ( k e. ( 1 ... n ) |-> A ) ( M ` ( E i^i y ) ) = sum* k e. ( 1 ... n ) ( M ` ( E i^i A ) ) )
182 153 163 181 3eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E i^i U_ k e. ( 1 ... n ) A ) ) = sum* k e. ( 1 ... n ) ( M ` ( E i^i A ) ) )
183 150 151 182 3eqtr3rd 
 |-  ( ( ph /\ n e. NN ) -> sum* k e. ( 1 ... n ) ( M ` ( E i^i A ) ) = ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) )
184 24 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. NN A ) ) e. ( 0 [,] +oo ) )
185 12 184 sseldi 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
186 185 xnegcld 
 |-  ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. NN A ) ) e. RR* )
187 22 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( M ` E ) e. RR* )
188 iunss1 
 |-  ( ( 1 ... n ) C_ NN -> U_ k e. ( 1 ... n ) A C_ U_ k e. NN A )
189 102 188 mp1i 
 |-  ( ( ph /\ n e. NN ) -> U_ k e. ( 1 ... n ) A C_ U_ k e. NN A )
190 189 sscond 
 |-  ( ( ph /\ n e. NN ) -> ( E \ U_ k e. NN A ) C_ ( E \ U_ k e. ( 1 ... n ) A ) )
191 5 3adant1r 
 |-  ( ( ( ph /\ n e. NN ) /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
192 109 79 190 86 191 carsgmon 
 |-  ( ( ph /\ n e. NN ) -> ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) )
193 xleneg 
 |-  ( ( ( M ` ( E \ U_ k e. NN A ) ) e. RR* /\ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* ) -> ( ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) <-> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) <_ -e ( M ` ( E \ U_ k e. NN A ) ) ) )
194 193 biimpa 
 |-  ( ( ( ( M ` ( E \ U_ k e. NN A ) ) e. RR* /\ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* ) /\ ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) -> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) <_ -e ( M ` ( E \ U_ k e. NN A ) ) )
195 185 88 192 194 syl21anc 
 |-  ( ( ph /\ n e. NN ) -> -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) <_ -e ( M ` ( E \ U_ k e. NN A ) ) )
196 xleadd2a 
 |-  ( ( ( -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) e. RR* /\ -e ( M ` ( E \ U_ k e. NN A ) ) e. RR* /\ ( M ` E ) e. RR* ) /\ -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) <_ -e ( M ` ( E \ U_ k e. NN A ) ) ) -> ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
197 91 186 187 195 196 syl31anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. ( 1 ... n ) A ) ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
198 183 197 eqbrtrd 
 |-  ( ( ph /\ n e. NN ) -> sum* k e. ( 1 ... n ) ( M ` ( E i^i A ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
199 78 29 198 esumgect 
 |-  ( ph -> sum* k e. NN ( M ` ( E i^i A ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
200 19 34 27 75 199 xrletrd 
 |-  ( ph -> ( M ` U_ k e. NN ( E i^i A ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
201 11 200 eqbrtrrid 
 |-  ( ph -> ( M ` ( E i^i U_ k e. NN A ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) )
202 xleadd1a 
 |-  ( ( ( ( M ` ( E i^i U_ k e. NN A ) ) e. RR* /\ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) e. RR* /\ ( M ` ( E \ U_ k e. NN A ) ) e. RR* ) /\ ( M ` ( E i^i U_ k e. NN A ) ) <_ ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) ) -> ( ( M ` ( E i^i U_ k e. NN A ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) <_ ( ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) )
203 20 27 25 201 202 syl31anc 
 |-  ( ph -> ( ( M ` ( E i^i U_ k e. NN A ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) <_ ( ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) )
204 xrge0npcan 
 |-  ( ( ( M ` E ) e. ( 0 [,] +oo ) /\ ( M ` ( E \ U_ k e. NN A ) ) e. ( 0 [,] +oo ) /\ ( M ` ( E \ U_ k e. NN A ) ) <_ ( M ` E ) ) -> ( ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) = ( M ` E ) )
205 21 24 77 204 syl3anc 
 |-  ( ph -> ( ( ( M ` E ) +e -e ( M ` ( E \ U_ k e. NN A ) ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) = ( M ` E ) )
206 203 205 breqtrd 
 |-  ( ph -> ( ( M ` ( E i^i U_ k e. NN A ) ) +e ( M ` ( E \ U_ k e. NN A ) ) ) <_ ( M ` E ) )