Metamath Proof Explorer


Theorem carsgsigalem

Description: Lemma for the following theorems. (Contributed by Thierry Arnoux, 23-May-2020)

Ref Expression
Hypotheses carsgval.1 φ O V
carsgval.2 φ M : 𝒫 O 0 +∞
carsgsiga.1 φ M = 0
carsgsiga.2 φ x ω x 𝒫 O M x * y x M y
Assertion carsgsigalem φ e 𝒫 O f 𝒫 O M e f M e + 𝑒 M f

Proof

Step Hyp Ref Expression
1 carsgval.1 φ O V
2 carsgval.2 φ M : 𝒫 O 0 +∞
3 carsgsiga.1 φ M = 0
4 carsgsiga.2 φ x ω x 𝒫 O M x * y x M y
5 simpr φ e 𝒫 O f 𝒫 O e = f e = f
6 5 uneq2d φ e 𝒫 O f 𝒫 O e = f e e = e f
7 unidm e e = e
8 6 7 eqtr3di φ e 𝒫 O f 𝒫 O e = f e f = e
9 8 fveq2d φ e 𝒫 O f 𝒫 O e = f M e f = M e
10 iccssxr 0 +∞ *
11 simp1 φ e 𝒫 O f 𝒫 O φ
12 11 2 syl φ e 𝒫 O f 𝒫 O M : 𝒫 O 0 +∞
13 simp2 φ e 𝒫 O f 𝒫 O e 𝒫 O
14 12 13 ffvelrnd φ e 𝒫 O f 𝒫 O M e 0 +∞
15 10 14 sselid φ e 𝒫 O f 𝒫 O M e *
16 15 adantr φ e 𝒫 O f 𝒫 O e = f M e *
17 5 fveq2d φ e 𝒫 O f 𝒫 O e = f M e = M f
18 17 16 eqeltrrd φ e 𝒫 O f 𝒫 O e = f M f *
19 simp3 φ e 𝒫 O f 𝒫 O f 𝒫 O
20 12 19 ffvelrnd φ e 𝒫 O f 𝒫 O M f 0 +∞
21 20 adantr φ e 𝒫 O f 𝒫 O e = f M f 0 +∞
22 elxrge0 M f 0 +∞ M f * 0 M f
23 22 simprbi M f 0 +∞ 0 M f
24 21 23 syl φ e 𝒫 O f 𝒫 O e = f 0 M f
25 xraddge02 M e * M f * 0 M f M e M e + 𝑒 M f
26 25 imp M e * M f * 0 M f M e M e + 𝑒 M f
27 16 18 24 26 syl21anc φ e 𝒫 O f 𝒫 O e = f M e M e + 𝑒 M f
28 9 27 eqbrtrd φ e 𝒫 O f 𝒫 O e = f M e f M e + 𝑒 M f
29 uniprg e 𝒫 O f 𝒫 O e f = e f
30 29 fveq2d e 𝒫 O f 𝒫 O M e f = M e f
31 30 3adant1 φ e 𝒫 O f 𝒫 O M e f = M e f
32 prct e 𝒫 O f 𝒫 O e f ω
33 32 3adant1 φ e 𝒫 O f 𝒫 O e f ω
34 prssi e 𝒫 O f 𝒫 O e f 𝒫 O
35 34 3adant1 φ e 𝒫 O f 𝒫 O e f 𝒫 O
36 prex e f V
37 breq1 x = e f x ω e f ω
38 sseq1 x = e f x 𝒫 O e f 𝒫 O
39 37 38 3anbi23d x = e f φ x ω x 𝒫 O φ e f ω e f 𝒫 O
40 unieq x = e f x = e f
41 40 fveq2d x = e f M x = M e f
42 esumeq1 x = e f * y x M y = * y e f M y
43 41 42 breq12d x = e f M x * y x M y M e f * y e f M y
44 39 43 imbi12d x = e f φ x ω x 𝒫 O M x * y x M y φ e f ω e f 𝒫 O M e f * y e f M y
45 44 4 vtoclg e f V φ e f ω e f 𝒫 O M e f * y e f M y
46 36 45 ax-mp φ e f ω e f 𝒫 O M e f * y e f M y
47 11 33 35 46 syl3anc φ e 𝒫 O f 𝒫 O M e f * y e f M y
48 31 47 eqbrtrrd φ e 𝒫 O f 𝒫 O M e f * y e f M y
49 48 adantr φ e 𝒫 O f 𝒫 O e f M e f * y e f M y
50 simpr φ e 𝒫 O f 𝒫 O y = e y = e
51 50 fveq2d φ e 𝒫 O f 𝒫 O y = e M y = M e
52 51 adantlr φ e 𝒫 O f 𝒫 O e f y = e M y = M e
53 simpr φ e 𝒫 O f 𝒫 O y = f y = f
54 53 fveq2d φ e 𝒫 O f 𝒫 O y = f M y = M f
55 54 adantlr φ e 𝒫 O f 𝒫 O e f y = f M y = M f
56 13 adantr φ e 𝒫 O f 𝒫 O e f e 𝒫 O
57 19 adantr φ e 𝒫 O f 𝒫 O e f f 𝒫 O
58 14 adantr φ e 𝒫 O f 𝒫 O e f M e 0 +∞
59 20 adantr φ e 𝒫 O f 𝒫 O e f M f 0 +∞
60 simpr φ e 𝒫 O f 𝒫 O e f e f
61 52 55 56 57 58 59 60 esumpr φ e 𝒫 O f 𝒫 O e f * y e f M y = M e + 𝑒 M f
62 49 61 breqtrd φ e 𝒫 O f 𝒫 O e f M e f M e + 𝑒 M f
63 28 62 pm2.61dane φ e 𝒫 O f 𝒫 O M e f M e + 𝑒 M f