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 ⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
xrge0slmod.2 ⊢ 𝑊 = ( 𝐺 ↾v ( 0 [,) +∞ ) )
Assertion xrge0slmod 𝑊 ∈ SLMod

Proof

Step Hyp Ref Expression
1 xrge0slmod.1 ⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
2 xrge0slmod.2 ⊢ 𝑊 = ( 𝐺 ↾v ( 0 [,) +∞ ) )
3 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
4 1 3 eqeltri ⊢ 𝐺 ∈ CMnd
5 ovex ⊢ ( 0 [,) +∞ ) ∈ V
6 2 resvcmn ⊢ ( ( 0 [,) +∞ ) ∈ V → ( 𝐺 ∈ CMnd ↔ 𝑊 ∈ CMnd ) )
7 5 6 ax-mp ⊢ ( 𝐺 ∈ CMnd ↔ 𝑊 ∈ CMnd )
8 4 7 mpbi ⊢ 𝑊 ∈ CMnd
9 rge0srg ⊢ ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ SRing
10 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
11 simplr ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑟 ∈ ( 0 [,) +∞ ) )
12 10 11 sseldi ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑟 ∈ ( 0 [,] +∞ ) )
13 simprr ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑤 ∈ ( 0 [,] +∞ ) )
14 ge0xmulcl ⊢ ( ( 𝑟 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) → ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) )
15 12 13 14 syl2anc ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) )
16 simprl ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑥 ∈ ( 0 [,] +∞ ) )
17 xrge0adddi ⊢ ( ( 𝑤 ∈ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑟 ∈ ( 0 [,] +∞ ) ) → ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) )
18 13 16 12 17 syl3anc ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) )
19 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
20 simpll ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑞 ∈ ( 0 [,) +∞ ) )
21 19 20 sseldi ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑞 ∈ ℝ )
22 19 11 sseldi ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑟 ∈ ℝ )
23 rexadd ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝑞 +𝑒 𝑟 ) = ( 𝑞 + 𝑟 ) )
24 21 22 23 syl2anc ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑞 +𝑒 𝑟 ) = ( 𝑞 + 𝑟 ) )
25 24 oveq1d ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 +𝑒 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) )
26 10 20 sseldi ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑞 ∈ ( 0 [,] +∞ ) )
27 xrge0adddir ⊢ ( ( 𝑞 ∈ ( 0 [,] +∞ ) ∧ 𝑟 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑞 +𝑒 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) )
28 26 12 13 27 syl3anc ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 +𝑒 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) )
29 25 28 eqtr3d ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) )
30 15 18 29 3jca ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) ∧ ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) ) )
31 rexmul ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝑞 ·e 𝑟 ) = ( 𝑞 · 𝑟 ) )
32 21 22 31 syl2anc ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑞 ·e 𝑟 ) = ( 𝑞 · 𝑟 ) )
33 32 oveq1d ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 ·e 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) )
34 21 rexrd ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑞 ∈ ℝ* )
35 22 rexrd ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑟 ∈ ℝ* )
36 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
37 36 13 sseldi ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑤 ∈ ℝ* )
38 xmulass ⊢ ( ( 𝑞 ∈ ℝ* ∧ 𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 𝑞 ·e 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) )
39 34 35 37 38 syl3anc ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 ·e 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) )
40 33 39 eqtr3d ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) )
41 xmulid2 ⊢ ( 𝑤 ∈ ℝ* → ( 1 ·e 𝑤 ) = 𝑤 )
42 37 41 syl ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 1 ·e 𝑤 ) = 𝑤 )
43 xmul02 ⊢ ( 𝑤 ∈ ℝ* → ( 0 ·e 𝑤 ) = 0 )
44 37 43 syl ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( 0 ·e 𝑤 ) = 0 )
45 40 42 44 3jca ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) ∧ ( 1 ·e 𝑤 ) = 𝑤 ∧ ( 0 ·e 𝑤 ) = 0 ) )
46 30 45 jca ⊢ ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → ( ( ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) ∧ ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) ) ∧ ( ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) ∧ ( 1 ·e 𝑤 ) = 𝑤 ∧ ( 0 ·e 𝑤 ) = 0 ) ) )
47 46 ralrimivva ⊢ ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑤 ∈ ( 0 [,] +∞ ) ( ( ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) ∧ ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) ) ∧ ( ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) ∧ ( 1 ·e 𝑤 ) = 𝑤 ∧ ( 0 ·e 𝑤 ) = 0 ) ) )
48 47 rgen2 ⊢ ∀ 𝑞 ∈ ( 0 [,) +∞ ) ∀ 𝑟 ∈ ( 0 [,) +∞ ) ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑤 ∈ ( 0 [,] +∞ ) ( ( ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) ∧ ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) ) ∧ ( ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) ∧ ( 1 ·e 𝑤 ) = 𝑤 ∧ ( 0 ·e 𝑤 ) = 0 ) )
49 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
50 1 fveq2i ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
51 49 50 eqtr4i ⊢ ( 0 [,] +∞ ) = ( Base ‘ 𝐺 )
52 2 51 resvbas ⊢ ( ( 0 [,) +∞ ) ∈ V → ( 0 [,] +∞ ) = ( Base ‘ 𝑊 ) )
53 5 52 ax-mp ⊢ ( 0 [,] +∞ ) = ( Base ‘ 𝑊 )
54 xrge0plusg ⊢ +𝑒 = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
55 1 fveq2i ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
56 54 55 eqtr4i ⊢ +𝑒 = ( +g ‘ 𝐺 )
57 2 56 resvplusg ⊢ ( ( 0 [,) +∞ ) ∈ V → +𝑒 = ( +g ‘ 𝑊 ) )
58 5 57 ax-mp ⊢ +𝑒 = ( +g ‘ 𝑊 )
59 ovex ⊢ ( 0 [,] +∞ ) ∈ V
60 ax-xrsvsca ⊢ ·e = ( ·𝑠 ‘ ℝ*𝑠 )
61 1 60 ressvsca ⊢ ( ( 0 [,] +∞ ) ∈ V → ·e = ( ·𝑠 ‘ 𝐺 ) )
62 59 61 ax-mp ⊢ ·e = ( ·𝑠 ‘ 𝐺 )
63 2 62 resvvsca ⊢ ( ( 0 [,) +∞ ) ∈ V → ·e = ( ·𝑠 ‘ 𝑊 ) )
64 5 63 ax-mp ⊢ ·e = ( ·𝑠 ‘ 𝑊 )
65 xrge00 ⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
66 1 fveq2i ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
67 65 66 eqtr4i ⊢ 0 = ( 0g ‘ 𝐺 )
68 2 67 resv0g ⊢ ( ( 0 [,) +∞ ) ∈ V → 0 = ( 0g ‘ 𝑊 ) )
69 5 68 ax-mp ⊢ 0 = ( 0g ‘ 𝑊 )
70 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
71 70 oveq1i ⊢ ( ℝfld ↾s ( 0 [,) +∞ ) ) = ( ( ℂfld ↾s ℝ ) ↾s ( 0 [,) +∞ ) )
72 reex ⊢ ℝ ∈ V
73 ressress ⊢ ( ( ℝ ∈ V ∧ ( 0 [,) +∞ ) ∈ V ) → ( ( ℂfld ↾s ℝ ) ↾s ( 0 [,) +∞ ) ) = ( ℂfld ↾s ( ℝ ∩ ( 0 [,) +∞ ) ) ) )
74 72 5 73 mp2an ⊢ ( ( ℂfld ↾s ℝ ) ↾s ( 0 [,) +∞ ) ) = ( ℂfld ↾s ( ℝ ∩ ( 0 [,) +∞ ) ) )
75 71 74 eqtri ⊢ ( ℝfld ↾s ( 0 [,) +∞ ) ) = ( ℂfld ↾s ( ℝ ∩ ( 0 [,) +∞ ) ) )
76 ax-xrssca ⊢ ℝfld = ( Scalar ‘ ℝ*𝑠 )
77 1 76 resssca ⊢ ( ( 0 [,] +∞ ) ∈ V → ℝfld = ( Scalar ‘ 𝐺 ) )
78 59 77 ax-mp ⊢ ℝfld = ( Scalar ‘ 𝐺 )
79 rebase ⊢ ℝ = ( Base ‘ ℝfld )
80 2 78 79 resvsca ⊢ ( ( 0 [,) +∞ ) ∈ V → ( ℝfld ↾s ( 0 [,) +∞ ) ) = ( Scalar ‘ 𝑊 ) )
81 5 80 ax-mp ⊢ ( ℝfld ↾s ( 0 [,) +∞ ) ) = ( Scalar ‘ 𝑊 )
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 ↾s ( ℝ ∩ ( 0 [,) +∞ ) ) ) = ( ℂfld ↾s ( 0 [,) +∞ ) )
87 75 81 86 3eqtr3ri ⊢ ( ℂfld ↾s ( 0 [,) +∞ ) ) = ( Scalar ‘ 𝑊 )
88 ax-resscn ⊢ ℝ ⊆ ℂ
89 19 88 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
90 eqid ⊢ ( ℂfld ↾s ( 0 [,) +∞ ) ) = ( ℂfld ↾s ( 0 [,) +∞ ) )
91 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
92 90 91 ressbas2 ⊢ ( ( 0 [,) +∞ ) ⊆ ℂ → ( 0 [,) +∞ ) = ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
93 89 92 ax-mp ⊢ ( 0 [,) +∞ ) = ( Base ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
94 cnfldadd ⊢ + = ( +g ‘ ℂfld )
95 90 94 ressplusg ⊢ ( ( 0 [,) +∞ ) ∈ V → + = ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
96 5 95 ax-mp ⊢ + = ( +g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
97 cnfldmul ⊢ · = ( .r ‘ ℂfld )
98 90 97 ressmulr ⊢ ( ( 0 [,) +∞ ) ∈ V → · = ( .r ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
99 5 98 ax-mp ⊢ · = ( .r ‘ ( ℂfld ↾s ( 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 = ( 1r ‘ ℂfld )
114 90 91 113 ress1r ⊢ ( ( ℂfld ∈ Ring ∧ 1 ∈ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → 1 = ( 1r ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
115 102 112 89 114 mp3an ⊢ 1 = ( 1r ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
116 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
117 100 101 116 mp2b ⊢ ℂfld ∈ Mnd
118 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
119 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
120 90 91 119 ress0g ⊢ ( ( ℂfld ∈ Mnd ∧ 0 ∈ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → 0 = ( 0g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) ) )
121 117 118 89 120 mp3an ⊢ 0 = ( 0g ‘ ( ℂfld ↾s ( 0 [,) +∞ ) ) )
122 53 58 64 69 87 93 96 99 115 121 isslmd ⊢ ( 𝑊 ∈ SLMod ↔ ( 𝑊 ∈ CMnd ∧ ( ℂfld ↾s ( 0 [,) +∞ ) ) ∈ SRing ∧ ∀ 𝑞 ∈ ( 0 [,) +∞ ) ∀ 𝑟 ∈ ( 0 [,) +∞ ) ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑤 ∈ ( 0 [,] +∞ ) ( ( ( 𝑟 ·e 𝑤 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑟 ·e ( 𝑤 +𝑒 𝑥 ) ) = ( ( 𝑟 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑥 ) ) ∧ ( ( 𝑞 + 𝑟 ) ·e 𝑤 ) = ( ( 𝑞 ·e 𝑤 ) +𝑒 ( 𝑟 ·e 𝑤 ) ) ) ∧ ( ( ( 𝑞 · 𝑟 ) ·e 𝑤 ) = ( 𝑞 ·e ( 𝑟 ·e 𝑤 ) ) ∧ ( 1 ·e 𝑤 ) = 𝑤 ∧ ( 0 ·e 𝑤 ) = 0 ) ) ) )
123 8 9 48 122 mpbir3an ⊢ 𝑊 ∈ SLMod