Metamath Proof Explorer


Theorem carsgclctunlem2

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

Ref Expression
Hypotheses carsgval.1 φOV
carsgval.2 φM:𝒫O0+∞
carsgsiga.1 φM=0
carsgsiga.2 φxωx𝒫OMx*yxMy
carsgsiga.3 φxyy𝒫OMxMy
carsgclctunlem2.1 φDisjkA
carsgclctunlem2.2 φkAtoCaraSigaM
carsgclctunlem2.3 φE𝒫O
carsgclctunlem2.4 φME+∞
Assertion carsgclctunlem2 φMEkA+𝑒MEkAME

Proof

Step Hyp Ref Expression
1 carsgval.1 φOV
2 carsgval.2 φM:𝒫O0+∞
3 carsgsiga.1 φM=0
4 carsgsiga.2 φxωx𝒫OMx*yxMy
5 carsgsiga.3 φxyy𝒫OMxMy
6 carsgclctunlem2.1 φDisjkA
7 carsgclctunlem2.2 φkAtoCaraSigaM
8 carsgclctunlem2.3 φE𝒫O
9 carsgclctunlem2.4 φME+∞
10 iunin2 kEA=EkA
11 10 fveq2i MkEA=MEkA
12 iccssxr 0+∞*
13 nnex V
14 13 a1i φV
15 8 adantr φkE𝒫O
16 15 elpwincl1 φkEA𝒫O
17 14 16 elpwiuncl φkEA𝒫O
18 2 17 ffvelrnd φMkEA0+∞
19 12 18 sselid φMkEA*
20 11 19 eqeltrrid φMEkA*
21 2 8 ffvelrnd φME0+∞
22 12 21 sselid φME*
23 8 elpwdifcl φEkA𝒫O
24 2 23 ffvelrnd φMEkA0+∞
25 12 24 sselid φMEkA*
26 25 xnegcld φMEkA*
27 22 26 xaddcld φME+𝑒MEkA*
28 2 adantr φkM:𝒫O0+∞
29 28 16 ffvelrnd φkMEA0+∞
30 29 ralrimiva φkMEA0+∞
31 nfcv _k
32 31 esumcl VkMEA0+∞*kMEA0+∞
33 14 30 32 syl2anc φ*kMEA0+∞
34 12 33 sselid φ*kMEA*
35 16 ralrimiva φkEA𝒫O
36 dfiun3g kEA𝒫OkEA=rankEA
37 35 36 syl φkEA=rankEA
38 37 fveq2d φMkEA=MrankEA
39 nnct ω
40 mptct ωkEAω
41 rnct kEAωrankEAω
42 39 40 41 mp2b rankEAω
43 42 a1i φrankEAω
44 eqid kEA=kEA
45 44 rnmptss kEA𝒫OrankEA𝒫O
46 35 45 syl φrankEA𝒫O
47 mptexg VkEAV
48 rnexg kEAVrankEAV
49 13 47 48 mp2b rankEAV
50 breq1 x=rankEAxωrankEAω
51 sseq1 x=rankEAx𝒫OrankEA𝒫O
52 50 51 3anbi23d x=rankEAφxωx𝒫OφrankEAωrankEA𝒫O
53 unieq x=rankEAx=rankEA
54 53 fveq2d x=rankEAMx=MrankEA
55 esumeq1 x=rankEA*yxMy=*yrankEAMy
56 54 55 breq12d x=rankEAMx*yxMyMrankEA*yrankEAMy
57 52 56 imbi12d x=rankEAφxωx𝒫OMx*yxMyφrankEAωrankEA𝒫OMrankEA*yrankEAMy
58 57 4 vtoclg rankEAVφrankEAωrankEA𝒫OMrankEA*yrankEAMy
59 49 58 ax-mp φrankEAωrankEA𝒫OMrankEA*yrankEAMy
60 43 46 59 mpd3an23 φMrankEA*yrankEAMy
61 38 60 eqbrtrd φMkEA*yrankEAMy
62 fveq2 y=EAMy=MEA
63 simpr φkEA=EA=
64 63 fveq2d φkEA=MEA=M
65 3 ad2antrr φkEA=M=0
66 64 65 eqtrd φkEA=MEA=0
67 disjin DisjkADisjkAE
68 6 67 syl φDisjkAE
69 incom AE=EA
70 69 rgenw kAE=EA
71 disjeq2 kAE=EADisjkAEDisjkEA
72 70 71 ax-mp DisjkAEDisjkEA
73 68 72 sylib φDisjkEA
74 62 14 29 16 66 73 esumrnmpt2 φ*yrankEAMy=*kMEA
75 61 74 breqtrd φMkEA*kMEA
76 difssd φEkAE
77 1 2 76 8 5 carsgmon φMEkAME
78 21 24 77 xrge0subcld φME+𝑒MEkA0+∞
79 2 adantr φnM:𝒫O0+∞
80 8 adantr φnE𝒫O
81 80 elpwincl1 φnEk=1nA𝒫O
82 79 81 ffvelrnd φnMEk=1nA0+∞
83 12 82 sselid φnMEk=1nA*
84 xrge0neqmnf MEk=1nA0+∞MEk=1nA−∞
85 82 84 syl φnMEk=1nA−∞
86 80 elpwdifcl φnEk=1nA𝒫O
87 79 86 ffvelrnd φnMEk=1nA0+∞
88 12 87 sselid φnMEk=1nA*
89 xrge0neqmnf MEk=1nA0+∞MEk=1nA−∞
90 87 89 syl φnMEk=1nA−∞
91 88 xnegcld φnMEk=1nA*
92 xnegneg MEk=1nA*MEk=1nA=MEk=1nA
93 88 92 syl φnMEk=1nA=MEk=1nA
94 93 adantr φnMEk=1nA=−∞MEk=1nA=MEk=1nA
95 xnegeq MEk=1nA=−∞MEk=1nA=−∞
96 95 adantl φnMEk=1nA=−∞MEk=1nA=−∞
97 xnegmnf −∞=+∞
98 96 97 eqtrdi φnMEk=1nA=−∞MEk=1nA=+∞
99 94 98 eqtr3d φnMEk=1nA=−∞MEk=1nA=+∞
100 99 oveq2d φnMEk=1nA=−∞MEk=1nA+𝑒MEk=1nA=MEk=1nA+𝑒+∞
101 simpll φnk1nφ
102 fz1ssnn 1n
103 102 a1i φn1n
104 103 sselda φnk1nk
105 101 104 7 syl2anc φnk1nAtoCaraSigaM
106 105 ralrimiva φnk1nAtoCaraSigaM
107 dfiun3g k1nAtoCaraSigaMk=1nA=rank1nA
108 106 107 syl φnk=1nA=rank1nA
109 1 adantr φnOV
110 3 adantr φnM=0
111 4 3adant1r φnxωx𝒫OMx*yxMy
112 fzfi 1nFin
113 mptfi 1nFink1nAFin
114 rnfi k1nAFinrank1nAFin
115 112 113 114 mp2b rank1nAFin
116 115 a1i φnrank1nAFin
117 eqid k1nA=k1nA
118 117 rnmptss k1nAtoCaraSigaMrank1nAtoCaraSigaM
119 106 118 syl φnrank1nAtoCaraSigaM
120 109 79 110 111 116 119 fiunelcarsg φnrank1nAtoCaraSigaM
121 108 120 eqeltrd φnk=1nAtoCaraSigaM
122 109 79 elcarsg φnk=1nAtoCaraSigaMk=1nAOe𝒫OMek=1nA+𝑒Mek=1nA=Me
123 121 122 mpbid φnk=1nAOe𝒫OMek=1nA+𝑒Mek=1nA=Me
124 123 simprd φne𝒫OMek=1nA+𝑒Mek=1nA=Me
125 ineq1 e=Eek=1nA=Ek=1nA
126 125 fveq2d e=EMek=1nA=MEk=1nA
127 difeq1 e=Eek=1nA=Ek=1nA
128 127 fveq2d e=EMek=1nA=MEk=1nA
129 126 128 oveq12d e=EMek=1nA+𝑒Mek=1nA=MEk=1nA+𝑒MEk=1nA
130 fveq2 e=EMe=ME
131 129 130 eqeq12d e=EMek=1nA+𝑒Mek=1nA=MeMEk=1nA+𝑒MEk=1nA=ME
132 131 rspcv E𝒫Oe𝒫OMek=1nA+𝑒Mek=1nA=MeMEk=1nA+𝑒MEk=1nA=ME
133 80 124 132 sylc φnMEk=1nA+𝑒MEk=1nA=ME
134 133 adantr φnMEk=1nA=−∞MEk=1nA+𝑒MEk=1nA=ME
135 xaddpnf1 MEk=1nA*MEk=1nA−∞MEk=1nA+𝑒+∞=+∞
136 83 85 135 syl2anc φnMEk=1nA+𝑒+∞=+∞
137 136 adantr φnMEk=1nA=−∞MEk=1nA+𝑒+∞=+∞
138 100 134 137 3eqtr3d φnMEk=1nA=−∞ME=+∞
139 9 ad2antrr φnMEk=1nA=−∞ME+∞
140 139 neneqd φnMEk=1nA=−∞¬ME=+∞
141 138 140 pm2.65da φn¬MEk=1nA=−∞
142 141 neqned φnMEk=1nA−∞
143 xaddass MEk=1nA*MEk=1nA−∞MEk=1nA*MEk=1nA−∞MEk=1nA*MEk=1nA−∞MEk=1nA+𝑒MEk=1nA+𝑒MEk=1nA=MEk=1nA+𝑒MEk=1nA+𝑒MEk=1nA
144 83 85 88 90 91 142 143 syl222anc φnMEk=1nA+𝑒MEk=1nA+𝑒MEk=1nA=MEk=1nA+𝑒MEk=1nA+𝑒MEk=1nA
145 xnegid MEk=1nA*MEk=1nA+𝑒MEk=1nA=0
146 88 145 syl φnMEk=1nA+𝑒MEk=1nA=0
147 146 oveq2d φnMEk=1nA+𝑒MEk=1nA+𝑒MEk=1nA=MEk=1nA+𝑒0
148 xaddid1 MEk=1nA*MEk=1nA+𝑒0=MEk=1nA
149 83 148 syl φnMEk=1nA+𝑒0=MEk=1nA
150 144 147 149 3eqtrd φnMEk=1nA+𝑒MEk=1nA+𝑒MEk=1nA=MEk=1nA
151 133 oveq1d φnMEk=1nA+𝑒MEk=1nA+𝑒MEk=1nA=ME+𝑒MEk=1nA
152 108 ineq2d φnEk=1nA=Erank1nA
153 152 fveq2d φnMEk=1nA=MErank1nA
154 mptss 1nk1nAkA
155 rnss k1nAkArank1nArankA
156 102 154 155 mp2b rank1nArankA
157 156 a1i φnrank1nArankA
158 disjrnmpt DisjkADisjyrankAy
159 6 158 syl φDisjyrankAy
160 159 adantr φnDisjyrankAy
161 disjss1 rank1nArankADisjyrankAyDisjyrank1nAy
162 157 160 161 sylc φnDisjyrank1nAy
163 109 79 110 111 116 119 162 80 carsgclctunlem1 φnMErank1nA=*yrank1nAMEy
164 ineq2 y=AEy=EA
165 164 fveq2d y=AMEy=MEA
166 112 elexi 1nV
167 166 a1i φn1nV
168 101 104 29 syl2anc φnk1nMEA0+∞
169 inss2 EAA
170 sseq2 A=EAAEA
171 169 170 mpbii A=EA
172 ss0 EAEA=
173 171 172 syl A=EA=
174 173 adantl φnk1nA=EA=
175 174 fveq2d φnk1nA=MEA=M
176 110 ad2antrr φnk1nA=M=0
177 175 176 eqtrd φnk1nA=MEA=0
178 6 adantr φnDisjkA
179 disjss1 1nDisjkADisjk=1nA
180 103 178 179 sylc φnDisjk=1nA
181 165 167 168 105 177 180 esumrnmpt2 φn*yrank1nAMEy=*k=1nMEA
182 153 163 181 3eqtrd φnMEk=1nA=*k=1nMEA
183 150 151 182 3eqtr3rd φn*k=1nMEA=ME+𝑒MEk=1nA
184 24 adantr φnMEkA0+∞
185 12 184 sselid φnMEkA*
186 185 xnegcld φnMEkA*
187 22 adantr φnME*
188 iunss1 1nk=1nAkA
189 102 188 mp1i φnk=1nAkA
190 189 sscond φnEkAEk=1nA
191 5 3adant1r φnxyy𝒫OMxMy
192 109 79 190 86 191 carsgmon φnMEkAMEk=1nA
193 xleneg MEkA*MEk=1nA*MEkAMEk=1nAMEk=1nAMEkA
194 193 biimpa MEkA*MEk=1nA*MEkAMEk=1nAMEk=1nAMEkA
195 185 88 192 194 syl21anc φnMEk=1nAMEkA
196 xleadd2a MEk=1nA*MEkA*ME*MEk=1nAMEkAME+𝑒MEk=1nAME+𝑒MEkA
197 91 186 187 195 196 syl31anc φnME+𝑒MEk=1nAME+𝑒MEkA
198 183 197 eqbrtrd φn*k=1nMEAME+𝑒MEkA
199 78 29 198 esumgect φ*kMEAME+𝑒MEkA
200 19 34 27 75 199 xrletrd φMkEAME+𝑒MEkA
201 11 200 eqbrtrrid φMEkAME+𝑒MEkA
202 xleadd1a MEkA*ME+𝑒MEkA*MEkA*MEkAME+𝑒MEkAMEkA+𝑒MEkAME+𝑒MEkA+𝑒MEkA
203 20 27 25 201 202 syl31anc φMEkA+𝑒MEkAME+𝑒MEkA+𝑒MEkA
204 xrge0npcan ME0+∞MEkA0+∞MEkAMEME+𝑒MEkA+𝑒MEkA=ME
205 21 24 77 204 syl3anc φME+𝑒MEkA+𝑒MEkA=ME
206 203 205 breqtrd φMEkA+𝑒MEkAME