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 sselid
 |-  ( ( ( 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 sselid
 |-  ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> q e. RR )
22 19 11 sselid
 |-  ( ( ( 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 sselid
 |-  ( ( ( 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 sselid
 |-  ( ( ( 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