Metamath Proof Explorer

Theorem xrge0slmod

Description: The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Hypotheses xrge0slmod.1 
|- G = ( RR*s |`s ( 0 [,] +oo ) )
xrge0slmod.2 
|- W = ( G |`v ( 0 [,) +oo ) )
Assertion xrge0slmod 
|- W e. SLMod

Proof

Step Hyp Ref Expression
1 xrge0slmod.1 
 |-  G = ( RR*s |`s ( 0 [,] +oo ) )
2 xrge0slmod.2 
 |-  W = ( G |`v ( 0 [,) +oo ) )
3 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
4 1 3 eqeltri 
 |-  G e. CMnd
5 ovex 
 |-  ( 0 [,) +oo ) e. _V
6 2 resvcmn 
 |-  ( ( 0 [,) +oo ) e. _V -> ( G e. CMnd <-> W e. CMnd ) )
7 5 6 ax-mp 
 |-  ( G e. CMnd <-> W e. CMnd )
8 4 7 mpbi 
 |-  W e. CMnd
9 rge0srg 
 |-  ( CCfld |`s ( 0 [,) +oo ) ) e. SRing
10 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
11 simplr 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> r e. ( 0 [,) +oo ) )
12 10 11 sseldi 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> r e. ( 0 [,] +oo ) )
13 simprr 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> w e. ( 0 [,] +oo ) )
14 ge0xmulcl 
 |-  ( ( r e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) -> ( r *e w ) e. ( 0 [,] +oo ) )
15 12 13 14 syl2anc 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( r *e w ) e. ( 0 [,] +oo ) )
16 simprl 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> x e. ( 0 [,] +oo ) )
17 xrge0adddi 
 |-  ( ( w e. ( 0 [,] +oo ) /\ x e. ( 0 [,] +oo ) /\ r e. ( 0 [,] +oo ) ) -> ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) )
18 13 16 12 17 syl3anc 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) )
19 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
20 simpll 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> q e. ( 0 [,) +oo ) )
21 19 20 sseldi 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> q e. RR )
22 19 11 sseldi 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> r e. RR )
23 rexadd 
 |-  ( ( q e. RR /\ r e. RR ) -> ( q +e r ) = ( q + r ) )
24 21 22 23 syl2anc 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( q +e r ) = ( q + r ) )
25 24 oveq1d 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q +e r ) *e w ) = ( ( q + r ) *e w ) )
26 10 20 sseldi 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> q e. ( 0 [,] +oo ) )
27 xrge0adddir 
 |-  ( ( q e. ( 0 [,] +oo ) /\ r e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) -> ( ( q +e r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) )
28 26 12 13 27 syl3anc 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q +e r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) )
29 25 28 eqtr3d 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) )
30 15 18 29 3jca 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( r *e w ) e. ( 0 [,] +oo ) /\ ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) /\ ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) )
31 rexmul 
 |-  ( ( q e. RR /\ r e. RR ) -> ( q *e r ) = ( q x. r ) )
32 21 22 31 syl2anc 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( q *e r ) = ( q x. r ) )
33 32 oveq1d 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q *e r ) *e w ) = ( ( q x. r ) *e w ) )
34 21 rexrd 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> q e. RR* )
35 22 rexrd 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> r e. RR* )
36 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
37 36 13 sseldi 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> w e. RR* )
38 xmulass 
 |-  ( ( q e. RR* /\ r e. RR* /\ w e. RR* ) -> ( ( q *e r ) *e w ) = ( q *e ( r *e w ) ) )
39 34 35 37 38 syl3anc 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q *e r ) *e w ) = ( q *e ( r *e w ) ) )
40 33 39 eqtr3d 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) )
41 xmulid2 
 |-  ( w e. RR* -> ( 1 *e w ) = w )
42 37 41 syl 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( 1 *e w ) = w )
43 xmul02 
 |-  ( w e. RR* -> ( 0 *e w ) = 0 )
44 37 43 syl 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( 0 *e w ) = 0 )
45 40 42 44 3jca 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) /\ ( 1 *e w ) = w /\ ( 0 *e w ) = 0 ) )
46 30 45 jca 
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( ( r *e w ) e. ( 0 [,] +oo ) /\ ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) /\ ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) /\ ( ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) /\ ( 1 *e w ) = w /\ ( 0 *e w ) = 0 ) ) )
47 46 ralrimivva 
 |-  ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) -> A. x e. ( 0 [,] +oo ) A. w e. ( 0 [,] +oo ) ( ( ( r *e w ) e. ( 0 [,] +oo ) /\ ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) /\ ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) /\ ( ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) /\ ( 1 *e w ) = w /\ ( 0 *e w ) = 0 ) ) )
48 47 rgen2 
 |-  A. q e. ( 0 [,) +oo ) A. r e. ( 0 [,) +oo ) A. x e. ( 0 [,] +oo ) A. w e. ( 0 [,] +oo ) ( ( ( r *e w ) e. ( 0 [,] +oo ) /\ ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) /\ ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) /\ ( ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) /\ ( 1 *e w ) = w /\ ( 0 *e w ) = 0 ) )
49 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
50 1 fveq2i 
 |-  ( Base ` G ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
51 49 50 eqtr4i 
 |-  ( 0 [,] +oo ) = ( Base ` G )
52 2 51 resvbas 
 |-  ( ( 0 [,) +oo ) e. _V -> ( 0 [,] +oo ) = ( Base ` W ) )
53 5 52 ax-mp 
 |-  ( 0 [,] +oo ) = ( Base ` W )
54 xrge0plusg 
 |-  +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
55 1 fveq2i 
 |-  ( +g ` G ) = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
56 54 55 eqtr4i 
 |-  +e = ( +g ` G )
57 2 56 resvplusg 
 |-  ( ( 0 [,) +oo ) e. _V -> +e = ( +g ` W ) )
58 5 57 ax-mp 
 |-  +e = ( +g ` W )
59 ovex 
 |-  ( 0 [,] +oo ) e. _V
60 ax-xrsvsca 
 |-  *e = ( .s ` RR*s )
61 1 60 ressvsca 
 |-  ( ( 0 [,] +oo ) e. _V -> *e = ( .s ` G ) )
62 59 61 ax-mp 
 |-  *e = ( .s ` G )
63 2 62 resvvsca 
 |-  ( ( 0 [,) +oo ) e. _V -> *e = ( .s ` W ) )
64 5 63 ax-mp 
 |-  *e = ( .s ` W )
65 xrge00 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
66 1 fveq2i 
 |-  ( 0g ` G ) = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
67 65 66 eqtr4i 
 |-  0 = ( 0g ` G )
68 2 67 resv0g 
 |-  ( ( 0 [,) +oo ) e. _V -> 0 = ( 0g ` W ) )
69 5 68 ax-mp 
 |-  0 = ( 0g ` W )
70 df-refld 
 |-  RRfld = ( CCfld |`s RR )
71 70 oveq1i 
 |-  ( RRfld |`s ( 0 [,) +oo ) ) = ( ( CCfld |`s RR ) |`s ( 0 [,) +oo ) )
72 reex 
 |-  RR e. _V
73 ressress 
 |-  ( ( RR e. _V /\ ( 0 [,) +oo ) e. _V ) -> ( ( CCfld |`s RR ) |`s ( 0 [,) +oo ) ) = ( CCfld |`s ( RR i^i ( 0 [,) +oo ) ) ) )
74 72 5 73 mp2an 
 |-  ( ( CCfld |`s RR ) |`s ( 0 [,) +oo ) ) = ( CCfld |`s ( RR i^i ( 0 [,) +oo ) ) )
75 71 74 eqtri 
 |-  ( RRfld |`s ( 0 [,) +oo ) ) = ( CCfld |`s ( RR i^i ( 0 [,) +oo ) ) )
76 ax-xrssca 
 |-  RRfld = ( Scalar ` RR*s )
77 1 76 resssca 
 |-  ( ( 0 [,] +oo ) e. _V -> RRfld = ( Scalar ` G ) )
78 59 77 ax-mp 
 |-  RRfld = ( Scalar ` G )
79 rebase 
 |-  RR = ( Base ` RRfld )
80 2 78 79 resvsca 
 |-  ( ( 0 [,) +oo ) e. _V -> ( RRfld |`s ( 0 [,) +oo ) ) = ( Scalar ` W ) )
81 5 80 ax-mp 
 |-  ( RRfld |`s ( 0 [,) +oo ) ) = ( Scalar ` W )
82 incom 
 |-  ( ( 0 [,) +oo ) i^i RR ) = ( RR i^i ( 0 [,) +oo ) )
83 df-ss 
 |-  ( ( 0 [,) +oo ) C_ RR <-> ( ( 0 [,) +oo ) i^i RR ) = ( 0 [,) +oo ) )
84 19 83 mpbi 
 |-  ( ( 0 [,) +oo ) i^i RR ) = ( 0 [,) +oo )
85 82 84 eqtr3i 
 |-  ( RR i^i ( 0 [,) +oo ) ) = ( 0 [,) +oo )
86 85 oveq2i 
 |-  ( CCfld |`s ( RR i^i ( 0 [,) +oo ) ) ) = ( CCfld |`s ( 0 [,) +oo ) )
87 75 81 86 3eqtr3ri 
 |-  ( CCfld |`s ( 0 [,) +oo ) ) = ( Scalar ` W )
88 ax-resscn 
 |-  RR C_ CC
89 19 88 sstri 
 |-  ( 0 [,) +oo ) C_ CC
90 eqid 
 |-  ( CCfld |`s ( 0 [,) +oo ) ) = ( CCfld |`s ( 0 [,) +oo ) )
91 cnfldbas 
 |-  CC = ( Base ` CCfld )
92 90 91 ressbas2 
 |-  ( ( 0 [,) +oo ) C_ CC -> ( 0 [,) +oo ) = ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
93 89 92 ax-mp 
 |-  ( 0 [,) +oo ) = ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) )
94 cnfldadd 
 |-  + = ( +g ` CCfld )
95 90 94 ressplusg 
 |-  ( ( 0 [,) +oo ) e. _V -> + = ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
96 5 95 ax-mp 
 |-  + = ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) )
97 cnfldmul 
 |-  x. = ( .r ` CCfld )
98 90 97 ressmulr 
 |-  ( ( 0 [,) +oo ) e. _V -> x. = ( .r ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
99 5 98 ax-mp 
 |-  x. = ( .r ` ( CCfld |`s ( 0 [,) +oo ) ) )
100 cndrng 
 |-  CCfld e. DivRing
101 drngring 
 |-  ( CCfld e. DivRing -> CCfld e. Ring )
102 100 101 ax-mp 
 |-  CCfld e. Ring
103 1re 
 |-  1 e. RR
104 0le1 
 |-  0 <_ 1
105 ltpnf 
 |-  ( 1 e. RR -> 1 < +oo )
106 103 105 ax-mp 
 |-  1 < +oo
107 103 104 106 3pm3.2i 
 |-  ( 1 e. RR /\ 0 <_ 1 /\ 1 < +oo )
108 0re 
 |-  0 e. RR
109 pnfxr 
 |-  +oo e. RR*
110 elico2 
 |-  ( ( 0 e. RR /\ +oo e. RR* ) -> ( 1 e. ( 0 [,) +oo ) <-> ( 1 e. RR /\ 0 <_ 1 /\ 1 < +oo ) ) )
111 108 109 110 mp2an 
 |-  ( 1 e. ( 0 [,) +oo ) <-> ( 1 e. RR /\ 0 <_ 1 /\ 1 < +oo ) )
112 107 111 mpbir 
 |-  1 e. ( 0 [,) +oo )
113 cnfld1 
 |-  1 = ( 1r ` CCfld )
114 90 91 113 ress1r 
 |-  ( ( CCfld e. Ring /\ 1 e. ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ CC ) -> 1 = ( 1r ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
115 102 112 89 114 mp3an 
 |-  1 = ( 1r ` ( CCfld |`s ( 0 [,) +oo ) ) )
116 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
117 100 101 116 mp2b 
 |-  CCfld e. Mnd
118 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
119 cnfld0 
 |-  0 = ( 0g ` CCfld )
120 90 91 119 ress0g 
 |-  ( ( CCfld e. Mnd /\ 0 e. ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ CC ) -> 0 = ( 0g ` ( CCfld |`s ( 0 [,) +oo ) ) ) )
121 117 118 89 120 mp3an 
 |-  0 = ( 0g ` ( CCfld |`s ( 0 [,) +oo ) ) )
122 53 58 64 69 87 93 96 99 115 121 isslmd 
 |-  ( W e. SLMod <-> ( W e. CMnd /\ ( CCfld |`s ( 0 [,) +oo ) ) e. SRing /\ A. q e. ( 0 [,) +oo ) A. r e. ( 0 [,) +oo ) A. x e. ( 0 [,] +oo ) A. w e. ( 0 [,] +oo ) ( ( ( r *e w ) e. ( 0 [,] +oo ) /\ ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) /\ ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) /\ ( ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) /\ ( 1 *e w ) = w /\ ( 0 *e w ) = 0 ) ) ) )
123 8 9 48 122 mpbir3an 
 |-  W e. SLMod