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 sseldi ⊢ 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 sseldi ⊢ q ∈ 0 +∞ ∧ r ∈ 0 +∞ ∧ x ∈ 0 +∞ ∧ w ∈ 0 +∞ → q ∈ ℝ
22 19 11 sseldi ⊢ 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 sseldi ⊢ 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 sseldi ⊢ 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 xmulid2 ⊢ 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 ⊢ Base G = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
51 49 50 eqtr4i ⊢ 0 +∞ = Base G
52 2 51 resvbas ⊢ 0 +∞ ∈ V → 0 +∞ = Base W
53 5 52 ax-mp ⊢ 0 +∞ = Base W
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 ⊢ 0 G = 0 ℝ 𝑠 * ↾ 𝑠 0 +∞
67 65 66 eqtr4i ⊢ 0 = 0 G
68 2 67 resv0g ⊢ 0 +∞ ∈ V → 0 = 0 W
69 5 68 ax-mp ⊢ 0 = 0 W
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