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 ( ℂflds ( 0 [,) +∞ ) ) ∈ SRing
10 icossicc ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
11 simplr ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑟 ∈ ( 0 [,) +∞ ) )
12 10 11 sselid ( ( ( 𝑞 ∈ ( 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 sselid ( ( ( 𝑞 ∈ ( 0 [,) +∞ ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑤 ∈ ( 0 [,] +∞ ) ) ) → 𝑞 ∈ ℝ )
22 19 11 sselid ( ( ( 𝑞 ∈ ( 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 sselid ( ( ( 𝑞 ∈ ( 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 sselid ( ( ( 𝑞 ∈ ( 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 = ( ℂflds ℝ )
71 70 oveq1i ( ℝflds ( 0 [,) +∞ ) ) = ( ( ℂflds ℝ ) ↾s ( 0 [,) +∞ ) )
72 reex ℝ ∈ V
73 ressress ( ( ℝ ∈ V ∧ ( 0 [,) +∞ ) ∈ V ) → ( ( ℂflds ℝ ) ↾s ( 0 [,) +∞ ) ) = ( ℂflds ( ℝ ∩ ( 0 [,) +∞ ) ) ) )
74 72 5 73 mp2an ( ( ℂflds ℝ ) ↾s ( 0 [,) +∞ ) ) = ( ℂflds ( ℝ ∩ ( 0 [,) +∞ ) ) )
75 71 74 eqtri ( ℝflds ( 0 [,) +∞ ) ) = ( ℂflds ( ℝ ∩ ( 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 → ( ℝflds ( 0 [,) +∞ ) ) = ( Scalar ‘ 𝑊 ) )
81 5 80 ax-mp ( ℝflds ( 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 ( ℂflds ( ℝ ∩ ( 0 [,) +∞ ) ) ) = ( ℂflds ( 0 [,) +∞ ) )
87 75 81 86 3eqtr3ri ( ℂflds ( 0 [,) +∞ ) ) = ( Scalar ‘ 𝑊 )
88 ax-resscn ℝ ⊆ ℂ
89 19 88 sstri ( 0 [,) +∞ ) ⊆ ℂ
90 eqid ( ℂflds ( 0 [,) +∞ ) ) = ( ℂflds ( 0 [,) +∞ ) )
91 cnfldbas ℂ = ( Base ‘ ℂfld )
92 90 91 ressbas2 ( ( 0 [,) +∞ ) ⊆ ℂ → ( 0 [,) +∞ ) = ( Base ‘ ( ℂflds ( 0 [,) +∞ ) ) ) )
93 89 92 ax-mp ( 0 [,) +∞ ) = ( Base ‘ ( ℂflds ( 0 [,) +∞ ) ) )
94 cnfldadd + = ( +g ‘ ℂfld )
95 90 94 ressplusg ( ( 0 [,) +∞ ) ∈ V → + = ( +g ‘ ( ℂflds ( 0 [,) +∞ ) ) ) )
96 5 95 ax-mp + = ( +g ‘ ( ℂflds ( 0 [,) +∞ ) ) )
97 cnfldmul · = ( .r ‘ ℂfld )
98 90 97 ressmulr ( ( 0 [,) +∞ ) ∈ V → · = ( .r ‘ ( ℂflds ( 0 [,) +∞ ) ) ) )
99 5 98 ax-mp · = ( .r ‘ ( ℂflds ( 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 ‘ ( ℂflds ( 0 [,) +∞ ) ) ) )
115 102 112 89 114 mp3an 1 = ( 1r ‘ ( ℂflds ( 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 ‘ ( ℂflds ( 0 [,) +∞ ) ) ) )
121 117 118 89 120 mp3an 0 = ( 0g ‘ ( ℂflds ( 0 [,) +∞ ) ) )
122 53 58 64 69 87 93 96 99 115 121 isslmd ( 𝑊 ∈ SLMod ↔ ( 𝑊 ∈ CMnd ∧ ( ℂflds ( 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