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
|
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 = ( ℂ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 |