Metamath Proof Explorer

Theorem carsgsigalem

Description: Lemma for the following theorems. (Contributed by Thierry Arnoux, 23-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 ) )
Assertion carsgsigalem 
|- ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> ( M ` ( e u. f ) ) <_ ( ( M ` e ) +e ( M ` f ) ) )

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 simpr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e = f ) -> e = f )
6 5 uneq2d 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e = f ) -> ( e u. e ) = ( e u. f ) )
7 unidm 
 |-  ( e u. e ) = e
8 6 7 eqtr3di 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e = f ) -> ( e u. f ) = e )
9 8 fveq2d 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e = f ) -> ( M ` ( e u. f ) ) = ( M ` e ) )
10 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
11 simp1 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> ph )
12 11 2 syl 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> M : ~P O --> ( 0 [,] +oo ) )
13 simp2 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> e e. ~P O )
14 12 13 ffvelrnd 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> ( M ` e ) e. ( 0 [,] +oo ) )
15 10 14 sselid 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> ( M ` e ) e. RR* )
16 15 adantr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e = f ) -> ( M ` e ) e. RR* )
17 5 fveq2d 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e = f ) -> ( M ` e ) = ( M ` f ) )
18 17 16 eqeltrrd 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e = f ) -> ( M ` f ) e. RR* )
19 simp3 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> f e. ~P O )
20 12 19 ffvelrnd 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> ( M ` f ) e. ( 0 [,] +oo ) )
21 20 adantr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e = f ) -> ( M ` f ) e. ( 0 [,] +oo ) )
22 elxrge0 
 |-  ( ( M ` f ) e. ( 0 [,] +oo ) <-> ( ( M ` f ) e. RR* /\ 0 <_ ( M ` f ) ) )
23 22 simprbi 
 |-  ( ( M ` f ) e. ( 0 [,] +oo ) -> 0 <_ ( M ` f ) )
24 21 23 syl 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e = f ) -> 0 <_ ( M ` f ) )
25 xraddge02 
 |-  ( ( ( M ` e ) e. RR* /\ ( M ` f ) e. RR* ) -> ( 0 <_ ( M ` f ) -> ( M ` e ) <_ ( ( M ` e ) +e ( M ` f ) ) ) )
26 25 imp 
 |-  ( ( ( ( M ` e ) e. RR* /\ ( M ` f ) e. RR* ) /\ 0 <_ ( M ` f ) ) -> ( M ` e ) <_ ( ( M ` e ) +e ( M ` f ) ) )
27 16 18 24 26 syl21anc 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e = f ) -> ( M ` e ) <_ ( ( M ` e ) +e ( M ` f ) ) )
28 9 27 eqbrtrd 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e = f ) -> ( M ` ( e u. f ) ) <_ ( ( M ` e ) +e ( M ` f ) ) )
29 uniprg 
 |-  ( ( e e. ~P O /\ f e. ~P O ) -> U. { e , f } = ( e u. f ) )
30 29 fveq2d 
 |-  ( ( e e. ~P O /\ f e. ~P O ) -> ( M ` U. { e , f } ) = ( M ` ( e u. f ) ) )
31 30 3adant1 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> ( M ` U. { e , f } ) = ( M ` ( e u. f ) ) )
32 prct 
 |-  ( ( e e. ~P O /\ f e. ~P O ) -> { e , f } ~<_ _om )
33 32 3adant1 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> { e , f } ~<_ _om )
34 prssi 
 |-  ( ( e e. ~P O /\ f e. ~P O ) -> { e , f } C_ ~P O )
35 34 3adant1 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> { e , f } C_ ~P O )
36 prex 
 |-  { e , f } e. _V
37 breq1 
 |-  ( x = { e , f } -> ( x ~<_ _om <-> { e , f } ~<_ _om ) )
38 sseq1 
 |-  ( x = { e , f } -> ( x C_ ~P O <-> { e , f } C_ ~P O ) )
39 37 38 3anbi23d 
 |-  ( x = { e , f } -> ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) <-> ( ph /\ { e , f } ~<_ _om /\ { e , f } C_ ~P O ) ) )
40 unieq 
 |-  ( x = { e , f } -> U. x = U. { e , f } )
41 40 fveq2d 
 |-  ( x = { e , f } -> ( M ` U. x ) = ( M ` U. { e , f } ) )
42 esumeq1 
 |-  ( x = { e , f } -> sum* y e. x ( M ` y ) = sum* y e. { e , f } ( M ` y ) )
43 41 42 breq12d 
 |-  ( x = { e , f } -> ( ( M ` U. x ) <_ sum* y e. x ( M ` y ) <-> ( M ` U. { e , f } ) <_ sum* y e. { e , f } ( M ` y ) ) )
44 39 43 imbi12d 
 |-  ( x = { e , f } -> ( ( ( ph /\ x ~<_ _om /\ x C_ ~P O ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) ) <-> ( ( ph /\ { e , f } ~<_ _om /\ { e , f } C_ ~P O ) -> ( M ` U. { e , f } ) <_ sum* y e. { e , f } ( M ` y ) ) ) )
45 44 4 vtoclg 
 |-  ( { e , f } e. _V -> ( ( ph /\ { e , f } ~<_ _om /\ { e , f } C_ ~P O ) -> ( M ` U. { e , f } ) <_ sum* y e. { e , f } ( M ` y ) ) )
46 36 45 ax-mp 
 |-  ( ( ph /\ { e , f } ~<_ _om /\ { e , f } C_ ~P O ) -> ( M ` U. { e , f } ) <_ sum* y e. { e , f } ( M ` y ) )
47 11 33 35 46 syl3anc 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> ( M ` U. { e , f } ) <_ sum* y e. { e , f } ( M ` y ) )
48 31 47 eqbrtrrd 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> ( M ` ( e u. f ) ) <_ sum* y e. { e , f } ( M ` y ) )
49 48 adantr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e =/= f ) -> ( M ` ( e u. f ) ) <_ sum* y e. { e , f } ( M ` y ) )
50 simpr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ y = e ) -> y = e )
51 50 fveq2d 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ y = e ) -> ( M ` y ) = ( M ` e ) )
52 51 adantlr 
 |-  ( ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e =/= f ) /\ y = e ) -> ( M ` y ) = ( M ` e ) )
53 simpr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ y = f ) -> y = f )
54 53 fveq2d 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ y = f ) -> ( M ` y ) = ( M ` f ) )
55 54 adantlr 
 |-  ( ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e =/= f ) /\ y = f ) -> ( M ` y ) = ( M ` f ) )
56 13 adantr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e =/= f ) -> e e. ~P O )
57 19 adantr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e =/= f ) -> f e. ~P O )
58 14 adantr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e =/= f ) -> ( M ` e ) e. ( 0 [,] +oo ) )
59 20 adantr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e =/= f ) -> ( M ` f ) e. ( 0 [,] +oo ) )
60 simpr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e =/= f ) -> e =/= f )
61 52 55 56 57 58 59 60 esumpr 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e =/= f ) -> sum* y e. { e , f } ( M ` y ) = ( ( M ` e ) +e ( M ` f ) ) )
62 49 61 breqtrd 
 |-  ( ( ( ph /\ e e. ~P O /\ f e. ~P O ) /\ e =/= f ) -> ( M ` ( e u. f ) ) <_ ( ( M ` e ) +e ( M ` f ) ) )
63 28 62 pm2.61dane 
 |-  ( ( ph /\ e e. ~P O /\ f e. ~P O ) -> ( M ` ( e u. f ) ) <_ ( ( M ` e ) +e ( M ` f ) ) )