Step | Hyp | Ref
| Expression |
1 | | xrge0slmod.1 |
. . . 4
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
2 | | xrge0cmn 20640 |
. . . 4
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
3 | 1, 2 | eqeltri 2835 |
. . 3
⊢ 𝐺 ∈ CMnd |
4 | | ovex 7308 |
. . . 4
⊢
(0[,)+∞) ∈ V |
5 | | xrge0slmod.2 |
. . . . 5
⊢ 𝑊 = (𝐺 ↾v
(0[,)+∞)) |
6 | 5 | resvcmn 31542 |
. . . 4
⊢
((0[,)+∞) ∈ V → (𝐺 ∈ CMnd ↔ 𝑊 ∈ CMnd)) |
7 | 4, 6 | ax-mp 5 |
. . 3
⊢ (𝐺 ∈ CMnd ↔ 𝑊 ∈ CMnd) |
8 | 3, 7 | mpbi 229 |
. 2
⊢ 𝑊 ∈ CMnd |
9 | | rge0srg 20669 |
. 2
⊢
(ℂfld ↾s (0[,)+∞)) ∈
SRing |
10 | | icossicc 13168 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
11 | | simplr 766 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑟 ∈ (0[,)+∞)) |
12 | 10, 11 | sselid 3919 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑟 ∈ (0[,]+∞)) |
13 | | simprr 770 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑤 ∈ (0[,]+∞)) |
14 | | ge0xmulcl 13195 |
. . . . . . 7
⊢ ((𝑟 ∈ (0[,]+∞) ∧
𝑤 ∈ (0[,]+∞))
→ (𝑟
·e 𝑤)
∈ (0[,]+∞)) |
15 | 12, 13, 14 | syl2anc 584 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (𝑟 ·e 𝑤) ∈ (0[,]+∞)) |
16 | | simprl 768 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑥 ∈ (0[,]+∞)) |
17 | | xrge0adddi 31302 |
. . . . . . 7
⊢ ((𝑤 ∈ (0[,]+∞) ∧
𝑥 ∈ (0[,]+∞)
∧ 𝑟 ∈
(0[,]+∞)) → (𝑟
·e (𝑤
+𝑒 𝑥)) =
((𝑟 ·e
𝑤) +𝑒
(𝑟 ·e
𝑥))) |
18 | 13, 16, 12, 17 | syl3anc 1370 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥))) |
19 | | rge0ssre 13188 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
20 | | simpll 764 |
. . . . . . . . . 10
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑞 ∈ (0[,)+∞)) |
21 | 19, 20 | sselid 3919 |
. . . . . . . . 9
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑞 ∈ ℝ) |
22 | 19, 11 | sselid 3919 |
. . . . . . . . 9
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑟 ∈ ℝ) |
23 | | rexadd 12966 |
. . . . . . . . 9
⊢ ((𝑞 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑞 +𝑒 𝑟) = (𝑞 + 𝑟)) |
24 | 21, 22, 23 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (𝑞 +𝑒 𝑟) = (𝑞 + 𝑟)) |
25 | 24 | oveq1d 7290 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 +𝑒 𝑟) ·e 𝑤) = ((𝑞 + 𝑟) ·e 𝑤)) |
26 | 10, 20 | sselid 3919 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑞 ∈ (0[,]+∞)) |
27 | | xrge0adddir 31301 |
. . . . . . . 8
⊢ ((𝑞 ∈ (0[,]+∞) ∧
𝑟 ∈ (0[,]+∞)
∧ 𝑤 ∈
(0[,]+∞)) → ((𝑞
+𝑒 𝑟)
·e 𝑤) =
((𝑞 ·e
𝑤) +𝑒
(𝑟 ·e
𝑤))) |
28 | 26, 12, 13, 27 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 +𝑒 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) |
29 | 25, 28 | eqtr3d 2780 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) |
30 | 15, 18, 29 | 3jca 1127 |
. . . . 5
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑟 ·e 𝑤) ∈ (0[,]+∞) ∧ (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤)))) |
31 | | rexmul 13005 |
. . . . . . . . 9
⊢ ((𝑞 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑞 ·e 𝑟) = (𝑞 · 𝑟)) |
32 | 21, 22, 31 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (𝑞 ·e 𝑟) = (𝑞 · 𝑟)) |
33 | 32 | oveq1d 7290 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 ·e 𝑟) ·e 𝑤) = ((𝑞 · 𝑟) ·e 𝑤)) |
34 | 21 | rexrd 11025 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑞 ∈ ℝ*) |
35 | 22 | rexrd 11025 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑟 ∈ ℝ*) |
36 | | iccssxr 13162 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
37 | 36, 13 | sselid 3919 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑤 ∈ ℝ*) |
38 | | xmulass 13021 |
. . . . . . . 8
⊢ ((𝑞 ∈ ℝ*
∧ 𝑟 ∈
ℝ* ∧ 𝑤
∈ ℝ*) → ((𝑞 ·e 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤))) |
39 | 34, 35, 37, 38 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 ·e 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤))) |
40 | 33, 39 | eqtr3d 2780 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤))) |
41 | | xmulid2 13014 |
. . . . . . 7
⊢ (𝑤 ∈ ℝ*
→ (1 ·e 𝑤) = 𝑤) |
42 | 37, 41 | syl 17 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (1 ·e 𝑤) = 𝑤) |
43 | | xmul02 13002 |
. . . . . . 7
⊢ (𝑤 ∈ ℝ*
→ (0 ·e 𝑤) = 0) |
44 | 37, 43 | syl 17 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (0 ·e 𝑤) = 0) |
45 | 40, 42, 44 | 3jca 1127 |
. . . . 5
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0)) |
46 | 30, 45 | jca 512 |
. . . 4
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (((𝑟 ·e 𝑤) ∈ (0[,]+∞) ∧ (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) ∧ (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0))) |
47 | 46 | ralrimivva 3123 |
. . 3
⊢ ((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
→ ∀𝑥 ∈
(0[,]+∞)∀𝑤
∈ (0[,]+∞)(((𝑟
·e 𝑤)
∈ (0[,]+∞) ∧ (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) ∧ (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0))) |
48 | 47 | rgen2 3120 |
. 2
⊢
∀𝑞 ∈
(0[,)+∞)∀𝑟
∈ (0[,)+∞)∀𝑥 ∈ (0[,]+∞)∀𝑤 ∈ (0[,]+∞)(((𝑟 ·e 𝑤) ∈ (0[,]+∞) ∧
(𝑟 ·e
(𝑤 +𝑒
𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) ∧ (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0)) |
49 | | xrge0base 31294 |
. . . . . 6
⊢
(0[,]+∞) = (Base‘(ℝ*𝑠
↾s (0[,]+∞))) |
50 | 1 | fveq2i 6777 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
51 | 49, 50 | eqtr4i 2769 |
. . . . 5
⊢
(0[,]+∞) = (Base‘𝐺) |
52 | 5, 51 | resvbas 31532 |
. . . 4
⊢
((0[,)+∞) ∈ V → (0[,]+∞) = (Base‘𝑊)) |
53 | 4, 52 | ax-mp 5 |
. . 3
⊢
(0[,]+∞) = (Base‘𝑊) |
54 | | xrge0plusg 31296 |
. . . . . 6
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
55 | 1 | fveq2i 6777 |
. . . . . 6
⊢
(+g‘𝐺) =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
56 | 54, 55 | eqtr4i 2769 |
. . . . 5
⊢
+𝑒 = (+g‘𝐺) |
57 | 5, 56 | resvplusg 31534 |
. . . 4
⊢
((0[,)+∞) ∈ V → +𝑒 =
(+g‘𝑊)) |
58 | 4, 57 | ax-mp 5 |
. . 3
⊢
+𝑒 = (+g‘𝑊) |
59 | | ovex 7308 |
. . . . . 6
⊢
(0[,]+∞) ∈ V |
60 | | ax-xrsvsca 31283 |
. . . . . . 7
⊢
·e = ( ·𝑠
‘ℝ*𝑠) |
61 | 1, 60 | ressvsca 17054 |
. . . . . 6
⊢
((0[,]+∞) ∈ V → ·e = (
·𝑠 ‘𝐺)) |
62 | 59, 61 | ax-mp 5 |
. . . . 5
⊢
·e = ( ·𝑠 ‘𝐺) |
63 | 5, 62 | resvvsca 31536 |
. . . 4
⊢
((0[,)+∞) ∈ V → ·e = (
·𝑠 ‘𝑊)) |
64 | 4, 63 | ax-mp 5 |
. . 3
⊢
·e = ( ·𝑠 ‘𝑊) |
65 | | xrge00 31295 |
. . . . . 6
⊢ 0 =
(0g‘(ℝ*𝑠
↾s (0[,]+∞))) |
66 | 1 | fveq2i 6777 |
. . . . . 6
⊢
(0g‘𝐺) =
(0g‘(ℝ*𝑠
↾s (0[,]+∞))) |
67 | 65, 66 | eqtr4i 2769 |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
68 | 5, 67 | resv0g 31540 |
. . . 4
⊢
((0[,)+∞) ∈ V → 0 = (0g‘𝑊)) |
69 | 4, 68 | ax-mp 5 |
. . 3
⊢ 0 =
(0g‘𝑊) |
70 | | df-refld 20810 |
. . . . . 6
⊢
ℝfld = (ℂfld ↾s
ℝ) |
71 | 70 | oveq1i 7285 |
. . . . 5
⊢
(ℝfld ↾s (0[,)+∞)) =
((ℂfld ↾s ℝ) ↾s
(0[,)+∞)) |
72 | | reex 10962 |
. . . . . 6
⊢ ℝ
∈ V |
73 | | ressress 16958 |
. . . . . 6
⊢ ((ℝ
∈ V ∧ (0[,)+∞) ∈ V) → ((ℂfld
↾s ℝ) ↾s (0[,)+∞)) =
(ℂfld ↾s (ℝ ∩
(0[,)+∞)))) |
74 | 72, 4, 73 | mp2an 689 |
. . . . 5
⊢
((ℂfld ↾s ℝ) ↾s
(0[,)+∞)) = (ℂfld ↾s (ℝ ∩
(0[,)+∞))) |
75 | 71, 74 | eqtri 2766 |
. . . 4
⊢
(ℝfld ↾s (0[,)+∞)) =
(ℂfld ↾s (ℝ ∩
(0[,)+∞))) |
76 | | ax-xrssca 31282 |
. . . . . . . 8
⊢
ℝfld =
(Scalar‘ℝ*𝑠) |
77 | 1, 76 | resssca 17053 |
. . . . . . 7
⊢
((0[,]+∞) ∈ V → ℝfld =
(Scalar‘𝐺)) |
78 | 59, 77 | ax-mp 5 |
. . . . . 6
⊢
ℝfld = (Scalar‘𝐺) |
79 | | rebase 20811 |
. . . . . 6
⊢ ℝ =
(Base‘ℝfld) |
80 | 5, 78, 79 | resvsca 31529 |
. . . . 5
⊢
((0[,)+∞) ∈ V → (ℝfld
↾s (0[,)+∞)) = (Scalar‘𝑊)) |
81 | 4, 80 | ax-mp 5 |
. . . 4
⊢
(ℝfld ↾s (0[,)+∞)) =
(Scalar‘𝑊) |
82 | | incom 4135 |
. . . . . 6
⊢
((0[,)+∞) ∩ ℝ) = (ℝ ∩
(0[,)+∞)) |
83 | | df-ss 3904 |
. . . . . . 7
⊢
((0[,)+∞) ⊆ ℝ ↔ ((0[,)+∞) ∩ ℝ) =
(0[,)+∞)) |
84 | 19, 83 | mpbi 229 |
. . . . . 6
⊢
((0[,)+∞) ∩ ℝ) = (0[,)+∞) |
85 | 82, 84 | eqtr3i 2768 |
. . . . 5
⊢ (ℝ
∩ (0[,)+∞)) = (0[,)+∞) |
86 | 85 | oveq2i 7286 |
. . . 4
⊢
(ℂfld ↾s (ℝ ∩
(0[,)+∞))) = (ℂfld ↾s
(0[,)+∞)) |
87 | 75, 81, 86 | 3eqtr3ri 2775 |
. . 3
⊢
(ℂfld ↾s (0[,)+∞)) =
(Scalar‘𝑊) |
88 | | ax-resscn 10928 |
. . . . 5
⊢ ℝ
⊆ ℂ |
89 | 19, 88 | sstri 3930 |
. . . 4
⊢
(0[,)+∞) ⊆ ℂ |
90 | | eqid 2738 |
. . . . 5
⊢
(ℂfld ↾s (0[,)+∞)) =
(ℂfld ↾s (0[,)+∞)) |
91 | | cnfldbas 20601 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
92 | 90, 91 | ressbas2 16949 |
. . . 4
⊢
((0[,)+∞) ⊆ ℂ → (0[,)+∞) =
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
93 | 89, 92 | ax-mp 5 |
. . 3
⊢
(0[,)+∞) = (Base‘(ℂfld ↾s
(0[,)+∞))) |
94 | | cnfldadd 20602 |
. . . . 5
⊢ + =
(+g‘ℂfld) |
95 | 90, 94 | ressplusg 17000 |
. . . 4
⊢
((0[,)+∞) ∈ V → + =
(+g‘(ℂfld ↾s
(0[,)+∞)))) |
96 | 4, 95 | ax-mp 5 |
. . 3
⊢ + =
(+g‘(ℂfld ↾s
(0[,)+∞))) |
97 | | cnfldmul 20603 |
. . . . 5
⊢ ·
= (.r‘ℂfld) |
98 | 90, 97 | ressmulr 17017 |
. . . 4
⊢
((0[,)+∞) ∈ V → · =
(.r‘(ℂfld ↾s
(0[,)+∞)))) |
99 | 4, 98 | ax-mp 5 |
. . 3
⊢ ·
= (.r‘(ℂfld ↾s
(0[,)+∞))) |
100 | | cndrng 20627 |
. . . . 5
⊢
ℂfld ∈ DivRing |
101 | | drngring 19998 |
. . . . 5
⊢
(ℂfld ∈ DivRing → ℂfld
∈ Ring) |
102 | 100, 101 | ax-mp 5 |
. . . 4
⊢
ℂfld ∈ Ring |
103 | | 1re 10975 |
. . . . . 6
⊢ 1 ∈
ℝ |
104 | | 0le1 11498 |
. . . . . 6
⊢ 0 ≤
1 |
105 | | ltpnf 12856 |
. . . . . . 7
⊢ (1 ∈
ℝ → 1 < +∞) |
106 | 103, 105 | ax-mp 5 |
. . . . . 6
⊢ 1 <
+∞ |
107 | 103, 104,
106 | 3pm3.2i 1338 |
. . . . 5
⊢ (1 ∈
ℝ ∧ 0 ≤ 1 ∧ 1 < +∞) |
108 | | 0re 10977 |
. . . . . 6
⊢ 0 ∈
ℝ |
109 | | pnfxr 11029 |
. . . . . 6
⊢ +∞
∈ ℝ* |
110 | | elico2 13143 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (1 ∈
(0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 <
+∞))) |
111 | 108, 109,
110 | mp2an 689 |
. . . . 5
⊢ (1 ∈
(0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 <
+∞)) |
112 | 107, 111 | mpbir 230 |
. . . 4
⊢ 1 ∈
(0[,)+∞) |
113 | | cnfld1 20623 |
. . . . 5
⊢ 1 =
(1r‘ℂfld) |
114 | 90, 91, 113 | ress1r 31486 |
. . . 4
⊢
((ℂfld ∈ Ring ∧ 1 ∈ (0[,)+∞) ∧
(0[,)+∞) ⊆ ℂ) → 1 =
(1r‘(ℂfld ↾s
(0[,)+∞)))) |
115 | 102, 112,
89, 114 | mp3an 1460 |
. . 3
⊢ 1 =
(1r‘(ℂfld ↾s
(0[,)+∞))) |
116 | | ringmnd 19793 |
. . . . 5
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
117 | 100, 101,
116 | mp2b 10 |
. . . 4
⊢
ℂfld ∈ Mnd |
118 | | 0e0icopnf 13190 |
. . . 4
⊢ 0 ∈
(0[,)+∞) |
119 | | cnfld0 20622 |
. . . . 5
⊢ 0 =
(0g‘ℂfld) |
120 | 90, 91, 119 | ress0g 18413 |
. . . 4
⊢
((ℂfld ∈ Mnd ∧ 0 ∈ (0[,)+∞) ∧
(0[,)+∞) ⊆ ℂ) → 0 =
(0g‘(ℂfld ↾s
(0[,)+∞)))) |
121 | 117, 118,
89, 120 | mp3an 1460 |
. . 3
⊢ 0 =
(0g‘(ℂfld ↾s
(0[,)+∞))) |
122 | 53, 58, 64, 69, 87, 93, 96, 99, 115, 121 | isslmd 31455 |
. 2
⊢ (𝑊 ∈ 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 1340 |
1
⊢ 𝑊 ∈ SLMod |