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=ℝ𝑠*↾𝑠0+∞
xrge0slmod.2 ⊢W=G↾𝑣0+∞
Assertion xrge0slmod ⊢W∈SLMod

Proof

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