Step | Hyp | Ref
| Expression |
1 | | cnring 19587 |
. . . 4
⊢
ℂfld ∈ Ring |
2 | | ringcmn 18404 |
. . . 4
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
3 | 1, 2 | ax-mp 5 |
. . 3
⊢
ℂfld ∈ CMnd |
4 | | rege0subm 19621 |
. . 3
⊢
(0[,)+∞) ∈
(SubMnd‘ℂfld) |
5 | | eqid 2610 |
. . . 4
⊢
(ℂfld ↾s (0[,)+∞)) =
(ℂfld ↾s (0[,)+∞)) |
6 | 5 | submcmn 18066 |
. . 3
⊢
((ℂfld ∈ CMnd ∧ (0[,)+∞) ∈
(SubMnd‘ℂfld)) → (ℂfld
↾s (0[,)+∞)) ∈ CMnd) |
7 | 3, 4, 6 | mp2an 704 |
. 2
⊢
(ℂfld ↾s (0[,)+∞)) ∈
CMnd |
8 | | rge0ssre 12151 |
. . . . 5
⊢
(0[,)+∞) ⊆ ℝ |
9 | | ax-resscn 9872 |
. . . . 5
⊢ ℝ
⊆ ℂ |
10 | 8, 9 | sstri 3577 |
. . . 4
⊢
(0[,)+∞) ⊆ ℂ |
11 | | 1re 9918 |
. . . . 5
⊢ 1 ∈
ℝ |
12 | | 0le1 10430 |
. . . . 5
⊢ 0 ≤
1 |
13 | | ltpnf 11830 |
. . . . . 6
⊢ (1 ∈
ℝ → 1 < +∞) |
14 | 11, 13 | ax-mp 5 |
. . . . 5
⊢ 1 <
+∞ |
15 | | 0re 9919 |
. . . . . 6
⊢ 0 ∈
ℝ |
16 | | pnfxr 9971 |
. . . . . 6
⊢ +∞
∈ ℝ* |
17 | | elico2 12108 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (1 ∈
(0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 <
+∞))) |
18 | 15, 16, 17 | mp2an 704 |
. . . . 5
⊢ (1 ∈
(0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 <
+∞)) |
19 | 11, 12, 14, 18 | mpbir3an 1237 |
. . . 4
⊢ 1 ∈
(0[,)+∞) |
20 | | ge0mulcl 12156 |
. . . . 5
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 · 𝑦) ∈
(0[,)+∞)) |
21 | 20 | rgen2a 2960 |
. . . 4
⊢
∀𝑥 ∈
(0[,)+∞)∀𝑦
∈ (0[,)+∞)(𝑥
· 𝑦) ∈
(0[,)+∞) |
22 | | eqid 2610 |
. . . . . 6
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
23 | 22 | ringmgp 18376 |
. . . . 5
⊢
(ℂfld ∈ Ring →
(mulGrp‘ℂfld) ∈ Mnd) |
24 | | cnfldbas 19571 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
25 | 22, 24 | mgpbas 18318 |
. . . . . 6
⊢ ℂ =
(Base‘(mulGrp‘ℂfld)) |
26 | | cnfld1 19590 |
. . . . . . 7
⊢ 1 =
(1r‘ℂfld) |
27 | 22, 26 | ringidval 18326 |
. . . . . 6
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
28 | | cnfldmul 19573 |
. . . . . . 7
⊢ ·
= (.r‘ℂfld) |
29 | 22, 28 | mgpplusg 18316 |
. . . . . 6
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
30 | 25, 27, 29 | issubm 17170 |
. . . . 5
⊢
((mulGrp‘ℂfld) ∈ Mnd → ((0[,)+∞)
∈ (SubMnd‘(mulGrp‘ℂfld)) ↔
((0[,)+∞) ⊆ ℂ ∧ 1 ∈ (0[,)+∞) ∧
∀𝑥 ∈
(0[,)+∞)∀𝑦
∈ (0[,)+∞)(𝑥
· 𝑦) ∈
(0[,)+∞)))) |
31 | 1, 23, 30 | mp2b 10 |
. . . 4
⊢
((0[,)+∞) ∈
(SubMnd‘(mulGrp‘ℂfld)) ↔ ((0[,)+∞)
⊆ ℂ ∧ 1 ∈ (0[,)+∞) ∧ ∀𝑥 ∈ (0[,)+∞)∀𝑦 ∈ (0[,)+∞)(𝑥 · 𝑦) ∈ (0[,)+∞))) |
32 | 10, 19, 21, 31 | mpbir3an 1237 |
. . 3
⊢
(0[,)+∞) ∈
(SubMnd‘(mulGrp‘ℂfld)) |
33 | | eqid 2610 |
. . . 4
⊢
((mulGrp‘ℂfld) ↾s
(0[,)+∞)) = ((mulGrp‘ℂfld) ↾s
(0[,)+∞)) |
34 | 33 | submmnd 17177 |
. . 3
⊢
((0[,)+∞) ∈
(SubMnd‘(mulGrp‘ℂfld)) →
((mulGrp‘ℂfld) ↾s (0[,)+∞))
∈ Mnd) |
35 | 32, 34 | ax-mp 5 |
. 2
⊢
((mulGrp‘ℂfld) ↾s
(0[,)+∞)) ∈ Mnd |
36 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑥
∈ (0[,)+∞)) |
37 | 10, 36 | sseldi 3566 |
. . . . . . . 8
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑥
∈ ℂ) |
38 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑦
∈ (0[,)+∞)) |
39 | 10, 38 | sseldi 3566 |
. . . . . . . 8
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑦
∈ ℂ) |
40 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑧
∈ (0[,)+∞)) |
41 | 10, 40 | sseldi 3566 |
. . . . . . . 8
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑧
∈ ℂ) |
42 | 37, 39, 41 | adddid 9943 |
. . . . . . 7
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → (𝑥
· (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) |
43 | 37, 39, 41 | adddird 9944 |
. . . . . . 7
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → ((𝑥
+ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
44 | 42, 43 | jca 553 |
. . . . . 6
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → ((𝑥
· (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) |
45 | 44 | ralrimiva 2949 |
. . . . 5
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ ∀𝑧 ∈
(0[,)+∞)((𝑥 ·
(𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) |
46 | 45 | ralrimiva 2949 |
. . . 4
⊢ (𝑥 ∈ (0[,)+∞) →
∀𝑦 ∈
(0[,)+∞)∀𝑧
∈ (0[,)+∞)((𝑥
· (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) |
47 | 10 | sseli 3564 |
. . . . 5
⊢ (𝑥 ∈ (0[,)+∞) →
𝑥 ∈
ℂ) |
48 | 47 | mul02d 10113 |
. . . 4
⊢ (𝑥 ∈ (0[,)+∞) → (0
· 𝑥) =
0) |
49 | 47 | mul01d 10114 |
. . . 4
⊢ (𝑥 ∈ (0[,)+∞) →
(𝑥 · 0) =
0) |
50 | 46, 48, 49 | jca32 556 |
. . 3
⊢ (𝑥 ∈ (0[,)+∞) →
(∀𝑦 ∈
(0[,)+∞)∀𝑧
∈ (0[,)+∞)((𝑥
· (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ ((0 · 𝑥) = 0 ∧ (𝑥 · 0) = 0))) |
51 | 50 | rgen 2906 |
. 2
⊢
∀𝑥 ∈
(0[,)+∞)(∀𝑦
∈ (0[,)+∞)∀𝑧 ∈ (0[,)+∞)((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ ((0 · 𝑥) = 0 ∧ (𝑥 · 0) = 0)) |
52 | 5, 24 | ressbas2 15758 |
. . . 4
⊢
((0[,)+∞) ⊆ ℂ → (0[,)+∞) =
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
53 | 10, 52 | ax-mp 5 |
. . 3
⊢
(0[,)+∞) = (Base‘(ℂfld ↾s
(0[,)+∞))) |
54 | | cnfldex 19570 |
. . . 4
⊢
ℂfld ∈ V |
55 | | ovex 6577 |
. . . 4
⊢
(0[,)+∞) ∈ V |
56 | 5, 22 | mgpress 18323 |
. . . 4
⊢
((ℂfld ∈ V ∧ (0[,)+∞) ∈ V) →
((mulGrp‘ℂfld) ↾s (0[,)+∞)) =
(mulGrp‘(ℂfld ↾s
(0[,)+∞)))) |
57 | 54, 55, 56 | mp2an 704 |
. . 3
⊢
((mulGrp‘ℂfld) ↾s
(0[,)+∞)) = (mulGrp‘(ℂfld ↾s
(0[,)+∞))) |
58 | | cnfldadd 19572 |
. . . . 5
⊢ + =
(+g‘ℂfld) |
59 | 5, 58 | ressplusg 15818 |
. . . 4
⊢
((0[,)+∞) ∈ V → + =
(+g‘(ℂfld ↾s
(0[,)+∞)))) |
60 | 55, 59 | ax-mp 5 |
. . 3
⊢ + =
(+g‘(ℂfld ↾s
(0[,)+∞))) |
61 | 5, 28 | ressmulr 15829 |
. . . 4
⊢
((0[,)+∞) ∈ V → · =
(.r‘(ℂfld ↾s
(0[,)+∞)))) |
62 | 55, 61 | ax-mp 5 |
. . 3
⊢ ·
= (.r‘(ℂfld ↾s
(0[,)+∞))) |
63 | | ringmnd 18379 |
. . . . 5
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
64 | 1, 63 | ax-mp 5 |
. . . 4
⊢
ℂfld ∈ Mnd |
65 | | 0e0icopnf 12153 |
. . . 4
⊢ 0 ∈
(0[,)+∞) |
66 | | cnfld0 19589 |
. . . . 5
⊢ 0 =
(0g‘ℂfld) |
67 | 5, 24, 66 | ress0g 17142 |
. . . 4
⊢
((ℂfld ∈ Mnd ∧ 0 ∈ (0[,)+∞) ∧
(0[,)+∞) ⊆ ℂ) → 0 =
(0g‘(ℂfld ↾s
(0[,)+∞)))) |
68 | 64, 65, 10, 67 | mp3an 1416 |
. . 3
⊢ 0 =
(0g‘(ℂfld ↾s
(0[,)+∞))) |
69 | 53, 57, 60, 62, 68 | issrg 18330 |
. 2
⊢
((ℂfld ↾s (0[,)+∞)) ∈ SRing
↔ ((ℂfld ↾s (0[,)+∞)) ∈ CMnd
∧ ((mulGrp‘ℂfld) ↾s (0[,)+∞))
∈ Mnd ∧ ∀𝑥
∈ (0[,)+∞)(∀𝑦 ∈ (0[,)+∞)∀𝑧 ∈ (0[,)+∞)((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ ((0 · 𝑥) = 0 ∧ (𝑥 · 0) = 0)))) |
70 | 7, 35, 51, 69 | mpbir3an 1237 |
1
⊢
(ℂfld ↾s (0[,)+∞)) ∈
SRing |