| Step | Hyp | Ref
| Expression |
| 1 | | xrge0slmod.1 |
. . . 4
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
| 2 | | xrge0cmn 21426 |
. . . 4
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
| 3 | 1, 2 | eqeltri 2837 |
. . 3
⊢ 𝐺 ∈ CMnd |
| 4 | | ovex 7464 |
. . . 4
⊢
(0[,)+∞) ∈ V |
| 5 | | xrge0slmod.2 |
. . . . 5
⊢ 𝑊 = (𝐺 ↾v
(0[,)+∞)) |
| 6 | 5 | resvcmn 33369 |
. . . 4
⊢
((0[,)+∞) ∈ V → (𝐺 ∈ CMnd ↔ 𝑊 ∈ CMnd)) |
| 7 | 4, 6 | ax-mp 5 |
. . 3
⊢ (𝐺 ∈ CMnd ↔ 𝑊 ∈ CMnd) |
| 8 | 3, 7 | mpbi 230 |
. 2
⊢ 𝑊 ∈ CMnd |
| 9 | | rge0srg 21456 |
. 2
⊢
(ℂfld ↾s (0[,)+∞)) ∈
SRing |
| 10 | | icossicc 13476 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
| 11 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑟 ∈ (0[,)+∞)) |
| 12 | 10, 11 | sselid 3981 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑟 ∈ (0[,]+∞)) |
| 13 | | simprr 773 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑤 ∈ (0[,]+∞)) |
| 14 | | ge0xmulcl 13503 |
. . . . . . 7
⊢ ((𝑟 ∈ (0[,]+∞) ∧
𝑤 ∈ (0[,]+∞))
→ (𝑟
·e 𝑤)
∈ (0[,]+∞)) |
| 15 | 12, 13, 14 | syl2anc 584 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (𝑟 ·e 𝑤) ∈ (0[,]+∞)) |
| 16 | | simprl 771 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑥 ∈ (0[,]+∞)) |
| 17 | | xrge0adddi 33024 |
. . . . . . 7
⊢ ((𝑤 ∈ (0[,]+∞) ∧
𝑥 ∈ (0[,]+∞)
∧ 𝑟 ∈
(0[,]+∞)) → (𝑟
·e (𝑤
+𝑒 𝑥)) =
((𝑟 ·e
𝑤) +𝑒
(𝑟 ·e
𝑥))) |
| 18 | 13, 16, 12, 17 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥))) |
| 19 | | rge0ssre 13496 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
| 20 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑞 ∈ (0[,)+∞)) |
| 21 | 19, 20 | sselid 3981 |
. . . . . . . . 9
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑞 ∈ ℝ) |
| 22 | 19, 11 | sselid 3981 |
. . . . . . . . 9
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑟 ∈ ℝ) |
| 23 | | rexadd 13274 |
. . . . . . . . 9
⊢ ((𝑞 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑞 +𝑒 𝑟) = (𝑞 + 𝑟)) |
| 24 | 21, 22, 23 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (𝑞 +𝑒 𝑟) = (𝑞 + 𝑟)) |
| 25 | 24 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 +𝑒 𝑟) ·e 𝑤) = ((𝑞 + 𝑟) ·e 𝑤)) |
| 26 | 10, 20 | sselid 3981 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑞 ∈ (0[,]+∞)) |
| 27 | | xrge0adddir 33023 |
. . . . . . . 8
⊢ ((𝑞 ∈ (0[,]+∞) ∧
𝑟 ∈ (0[,]+∞)
∧ 𝑤 ∈
(0[,]+∞)) → ((𝑞
+𝑒 𝑟)
·e 𝑤) =
((𝑞 ·e
𝑤) +𝑒
(𝑟 ·e
𝑤))) |
| 28 | 26, 12, 13, 27 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 +𝑒 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) |
| 29 | 25, 28 | eqtr3d 2779 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) |
| 30 | 15, 18, 29 | 3jca 1129 |
. . . . 5
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑟 ·e 𝑤) ∈ (0[,]+∞) ∧ (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤)))) |
| 31 | | rexmul 13313 |
. . . . . . . . 9
⊢ ((𝑞 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑞 ·e 𝑟) = (𝑞 · 𝑟)) |
| 32 | 21, 22, 31 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (𝑞 ·e 𝑟) = (𝑞 · 𝑟)) |
| 33 | 32 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 ·e 𝑟) ·e 𝑤) = ((𝑞 · 𝑟) ·e 𝑤)) |
| 34 | 21 | rexrd 11311 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑞 ∈ ℝ*) |
| 35 | 22 | rexrd 11311 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑟 ∈ ℝ*) |
| 36 | | iccssxr 13470 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
| 37 | 36, 13 | sselid 3981 |
. . . . . . . 8
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → 𝑤 ∈ ℝ*) |
| 38 | | xmulass 13329 |
. . . . . . . 8
⊢ ((𝑞 ∈ ℝ*
∧ 𝑟 ∈
ℝ* ∧ 𝑤
∈ ℝ*) → ((𝑞 ·e 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤))) |
| 39 | 34, 35, 37, 38 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 ·e 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤))) |
| 40 | 33, 39 | eqtr3d 2779 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → ((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤))) |
| 41 | | xmullid 13322 |
. . . . . . 7
⊢ (𝑤 ∈ ℝ*
→ (1 ·e 𝑤) = 𝑤) |
| 42 | 37, 41 | syl 17 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (1 ·e 𝑤) = 𝑤) |
| 43 | | xmul02 13310 |
. . . . . . 7
⊢ (𝑤 ∈ ℝ*
→ (0 ·e 𝑤) = 0) |
| 44 | 37, 43 | syl 17 |
. . . . . 6
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (0 ·e 𝑤) = 0) |
| 45 | 40, 42, 44 | 3jca 1129 |
. . . . 5
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0)) |
| 46 | 30, 45 | jca 511 |
. . . 4
⊢ (((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
∧ (𝑥 ∈
(0[,]+∞) ∧ 𝑤
∈ (0[,]+∞))) → (((𝑟 ·e 𝑤) ∈ (0[,]+∞) ∧ (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) ∧ (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0))) |
| 47 | 46 | ralrimivva 3202 |
. . 3
⊢ ((𝑞 ∈ (0[,)+∞) ∧
𝑟 ∈ (0[,)+∞))
→ ∀𝑥 ∈
(0[,]+∞)∀𝑤
∈ (0[,]+∞)(((𝑟
·e 𝑤)
∈ (0[,]+∞) ∧ (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) ∧ (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0))) |
| 48 | 47 | rgen2 3199 |
. 2
⊢
∀𝑞 ∈
(0[,)+∞)∀𝑟
∈ (0[,)+∞)∀𝑥 ∈ (0[,]+∞)∀𝑤 ∈ (0[,]+∞)(((𝑟 ·e 𝑤) ∈ (0[,]+∞) ∧
(𝑟 ·e
(𝑤 +𝑒
𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) ∧ (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0)) |
| 49 | | xrge0base 33016 |
. . . . . 6
⊢
(0[,]+∞) = (Base‘(ℝ*𝑠
↾s (0[,]+∞))) |
| 50 | 1 | fveq2i 6909 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
| 51 | 49, 50 | eqtr4i 2768 |
. . . . 5
⊢
(0[,]+∞) = (Base‘𝐺) |
| 52 | 5, 51 | resvbas 33359 |
. . . 4
⊢
((0[,)+∞) ∈ V → (0[,]+∞) = (Base‘𝑊)) |
| 53 | 4, 52 | ax-mp 5 |
. . 3
⊢
(0[,]+∞) = (Base‘𝑊) |
| 54 | | xrge0plusg 33018 |
. . . . . 6
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
| 55 | 1 | fveq2i 6909 |
. . . . . 6
⊢
(+g‘𝐺) =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
| 56 | 54, 55 | eqtr4i 2768 |
. . . . 5
⊢
+𝑒 = (+g‘𝐺) |
| 57 | 5, 56 | resvplusg 33361 |
. . . 4
⊢
((0[,)+∞) ∈ V → +𝑒 =
(+g‘𝑊)) |
| 58 | 4, 57 | ax-mp 5 |
. . 3
⊢
+𝑒 = (+g‘𝑊) |
| 59 | | ovex 7464 |
. . . . . 6
⊢
(0[,]+∞) ∈ V |
| 60 | | ax-xrsvsca 33007 |
. . . . . . 7
⊢
·e = ( ·𝑠
‘ℝ*𝑠) |
| 61 | 1, 60 | ressvsca 17388 |
. . . . . 6
⊢
((0[,]+∞) ∈ V → ·e = (
·𝑠 ‘𝐺)) |
| 62 | 59, 61 | ax-mp 5 |
. . . . 5
⊢
·e = ( ·𝑠 ‘𝐺) |
| 63 | 5, 62 | resvvsca 33363 |
. . . 4
⊢
((0[,)+∞) ∈ V → ·e = (
·𝑠 ‘𝑊)) |
| 64 | 4, 63 | ax-mp 5 |
. . 3
⊢
·e = ( ·𝑠 ‘𝑊) |
| 65 | | xrge00 33017 |
. . . . . 6
⊢ 0 =
(0g‘(ℝ*𝑠
↾s (0[,]+∞))) |
| 66 | 1 | fveq2i 6909 |
. . . . . 6
⊢
(0g‘𝐺) =
(0g‘(ℝ*𝑠
↾s (0[,]+∞))) |
| 67 | 65, 66 | eqtr4i 2768 |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
| 68 | 5, 67 | resv0g 33367 |
. . . 4
⊢
((0[,)+∞) ∈ V → 0 = (0g‘𝑊)) |
| 69 | 4, 68 | ax-mp 5 |
. . 3
⊢ 0 =
(0g‘𝑊) |
| 70 | | df-refld 21623 |
. . . . . 6
⊢
ℝfld = (ℂfld ↾s
ℝ) |
| 71 | 70 | oveq1i 7441 |
. . . . 5
⊢
(ℝfld ↾s (0[,)+∞)) =
((ℂfld ↾s ℝ) ↾s
(0[,)+∞)) |
| 72 | | reex 11246 |
. . . . . 6
⊢ ℝ
∈ V |
| 73 | | ressress 17293 |
. . . . . 6
⊢ ((ℝ
∈ V ∧ (0[,)+∞) ∈ V) → ((ℂfld
↾s ℝ) ↾s (0[,)+∞)) =
(ℂfld ↾s (ℝ ∩
(0[,)+∞)))) |
| 74 | 72, 4, 73 | mp2an 692 |
. . . . 5
⊢
((ℂfld ↾s ℝ) ↾s
(0[,)+∞)) = (ℂfld ↾s (ℝ ∩
(0[,)+∞))) |
| 75 | 71, 74 | eqtri 2765 |
. . . 4
⊢
(ℝfld ↾s (0[,)+∞)) =
(ℂfld ↾s (ℝ ∩
(0[,)+∞))) |
| 76 | | ax-xrssca 33006 |
. . . . . . . 8
⊢
ℝfld =
(Scalar‘ℝ*𝑠) |
| 77 | 1, 76 | resssca 17387 |
. . . . . . 7
⊢
((0[,]+∞) ∈ V → ℝfld =
(Scalar‘𝐺)) |
| 78 | 59, 77 | ax-mp 5 |
. . . . . 6
⊢
ℝfld = (Scalar‘𝐺) |
| 79 | | rebase 21624 |
. . . . . 6
⊢ ℝ =
(Base‘ℝfld) |
| 80 | 5, 78, 79 | resvsca 33356 |
. . . . 5
⊢
((0[,)+∞) ∈ V → (ℝfld
↾s (0[,)+∞)) = (Scalar‘𝑊)) |
| 81 | 4, 80 | ax-mp 5 |
. . . 4
⊢
(ℝfld ↾s (0[,)+∞)) =
(Scalar‘𝑊) |
| 82 | | incom 4209 |
. . . . . 6
⊢
((0[,)+∞) ∩ ℝ) = (ℝ ∩
(0[,)+∞)) |
| 83 | | dfss2 3969 |
. . . . . . 7
⊢
((0[,)+∞) ⊆ ℝ ↔ ((0[,)+∞) ∩ ℝ) =
(0[,)+∞)) |
| 84 | 19, 83 | mpbi 230 |
. . . . . 6
⊢
((0[,)+∞) ∩ ℝ) = (0[,)+∞) |
| 85 | 82, 84 | eqtr3i 2767 |
. . . . 5
⊢ (ℝ
∩ (0[,)+∞)) = (0[,)+∞) |
| 86 | 85 | oveq2i 7442 |
. . . 4
⊢
(ℂfld ↾s (ℝ ∩
(0[,)+∞))) = (ℂfld ↾s
(0[,)+∞)) |
| 87 | 75, 81, 86 | 3eqtr3ri 2774 |
. . 3
⊢
(ℂfld ↾s (0[,)+∞)) =
(Scalar‘𝑊) |
| 88 | | ax-resscn 11212 |
. . . . 5
⊢ ℝ
⊆ ℂ |
| 89 | 19, 88 | sstri 3993 |
. . . 4
⊢
(0[,)+∞) ⊆ ℂ |
| 90 | | eqid 2737 |
. . . . 5
⊢
(ℂfld ↾s (0[,)+∞)) =
(ℂfld ↾s (0[,)+∞)) |
| 91 | | cnfldbas 21368 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
| 92 | 90, 91 | ressbas2 17283 |
. . . 4
⊢
((0[,)+∞) ⊆ ℂ → (0[,)+∞) =
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
| 93 | 89, 92 | ax-mp 5 |
. . 3
⊢
(0[,)+∞) = (Base‘(ℂfld ↾s
(0[,)+∞))) |
| 94 | | cnfldadd 21370 |
. . . . 5
⊢ + =
(+g‘ℂfld) |
| 95 | 90, 94 | ressplusg 17334 |
. . . 4
⊢
((0[,)+∞) ∈ V → + =
(+g‘(ℂfld ↾s
(0[,)+∞)))) |
| 96 | 4, 95 | ax-mp 5 |
. . 3
⊢ + =
(+g‘(ℂfld ↾s
(0[,)+∞))) |
| 97 | | cnfldmul 21372 |
. . . . 5
⊢ ·
= (.r‘ℂfld) |
| 98 | 90, 97 | ressmulr 17351 |
. . . 4
⊢
((0[,)+∞) ∈ V → · =
(.r‘(ℂfld ↾s
(0[,)+∞)))) |
| 99 | 4, 98 | ax-mp 5 |
. . 3
⊢ ·
= (.r‘(ℂfld ↾s
(0[,)+∞))) |
| 100 | | cndrng 21411 |
. . . . 5
⊢
ℂfld ∈ DivRing |
| 101 | | drngring 20736 |
. . . . 5
⊢
(ℂfld ∈ DivRing → ℂfld
∈ Ring) |
| 102 | 100, 101 | ax-mp 5 |
. . . 4
⊢
ℂfld ∈ Ring |
| 103 | | 1re 11261 |
. . . . . 6
⊢ 1 ∈
ℝ |
| 104 | | 0le1 11786 |
. . . . . 6
⊢ 0 ≤
1 |
| 105 | | ltpnf 13162 |
. . . . . . 7
⊢ (1 ∈
ℝ → 1 < +∞) |
| 106 | 103, 105 | ax-mp 5 |
. . . . . 6
⊢ 1 <
+∞ |
| 107 | 103, 104,
106 | 3pm3.2i 1340 |
. . . . 5
⊢ (1 ∈
ℝ ∧ 0 ≤ 1 ∧ 1 < +∞) |
| 108 | | 0re 11263 |
. . . . . 6
⊢ 0 ∈
ℝ |
| 109 | | pnfxr 11315 |
. . . . . 6
⊢ +∞
∈ ℝ* |
| 110 | | elico2 13451 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (1 ∈
(0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 <
+∞))) |
| 111 | 108, 109,
110 | mp2an 692 |
. . . . 5
⊢ (1 ∈
(0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 <
+∞)) |
| 112 | 107, 111 | mpbir 231 |
. . . 4
⊢ 1 ∈
(0[,)+∞) |
| 113 | | cnfld1 21406 |
. . . . 5
⊢ 1 =
(1r‘ℂfld) |
| 114 | 90, 91, 113 | ress1r 33238 |
. . . 4
⊢
((ℂfld ∈ Ring ∧ 1 ∈ (0[,)+∞) ∧
(0[,)+∞) ⊆ ℂ) → 1 =
(1r‘(ℂfld ↾s
(0[,)+∞)))) |
| 115 | 102, 112,
89, 114 | mp3an 1463 |
. . 3
⊢ 1 =
(1r‘(ℂfld ↾s
(0[,)+∞))) |
| 116 | | ringmnd 20240 |
. . . . 5
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
| 117 | 100, 101,
116 | mp2b 10 |
. . . 4
⊢
ℂfld ∈ Mnd |
| 118 | | 0e0icopnf 13498 |
. . . 4
⊢ 0 ∈
(0[,)+∞) |
| 119 | | cnfld0 21405 |
. . . . 5
⊢ 0 =
(0g‘ℂfld) |
| 120 | 90, 91, 119 | ress0g 18775 |
. . . 4
⊢
((ℂfld ∈ Mnd ∧ 0 ∈ (0[,)+∞) ∧
(0[,)+∞) ⊆ ℂ) → 0 =
(0g‘(ℂfld ↾s
(0[,)+∞)))) |
| 121 | 117, 118,
89, 120 | mp3an 1463 |
. . 3
⊢ 0 =
(0g‘(ℂfld ↾s
(0[,)+∞))) |
| 122 | 53, 58, 64, 69, 87, 93, 96, 99, 115, 121 | isslmd 33208 |
. 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 1342 |
1
⊢ 𝑊 ∈ SLMod |