| Step | Hyp | Ref
| Expression |
| 1 | | cnring 21403 |
. . . 4
⊢
ℂfld ∈ Ring |
| 2 | | ringcmn 20279 |
. . . 4
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
| 3 | 1, 2 | ax-mp 5 |
. . 3
⊢
ℂfld ∈ CMnd |
| 4 | | rege0subm 21441 |
. . 3
⊢
(0[,)+∞) ∈
(SubMnd‘ℂfld) |
| 5 | | eqid 2737 |
. . . 4
⊢
(ℂfld ↾s (0[,)+∞)) =
(ℂfld ↾s (0[,)+∞)) |
| 6 | 5 | submcmn 19856 |
. . 3
⊢
((ℂfld ∈ CMnd ∧ (0[,)+∞) ∈
(SubMnd‘ℂfld)) → (ℂfld
↾s (0[,)+∞)) ∈ CMnd) |
| 7 | 3, 4, 6 | mp2an 692 |
. 2
⊢
(ℂfld ↾s (0[,)+∞)) ∈
CMnd |
| 8 | | rge0ssre 13496 |
. . . . 5
⊢
(0[,)+∞) ⊆ ℝ |
| 9 | | ax-resscn 11212 |
. . . . 5
⊢ ℝ
⊆ ℂ |
| 10 | 8, 9 | sstri 3993 |
. . . 4
⊢
(0[,)+∞) ⊆ ℂ |
| 11 | | 1re 11261 |
. . . . 5
⊢ 1 ∈
ℝ |
| 12 | | 0le1 11786 |
. . . . 5
⊢ 0 ≤
1 |
| 13 | | ltpnf 13162 |
. . . . . 6
⊢ (1 ∈
ℝ → 1 < +∞) |
| 14 | 11, 13 | ax-mp 5 |
. . . . 5
⊢ 1 <
+∞ |
| 15 | | 0re 11263 |
. . . . . 6
⊢ 0 ∈
ℝ |
| 16 | | pnfxr 11315 |
. . . . . 6
⊢ +∞
∈ ℝ* |
| 17 | | elico2 13451 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (1 ∈
(0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 <
+∞))) |
| 18 | 15, 16, 17 | mp2an 692 |
. . . . 5
⊢ (1 ∈
(0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 <
+∞)) |
| 19 | 11, 12, 14, 18 | mpbir3an 1342 |
. . . 4
⊢ 1 ∈
(0[,)+∞) |
| 20 | | ge0mulcl 13501 |
. . . . 5
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 · 𝑦) ∈
(0[,)+∞)) |
| 21 | 20 | rgen2 3199 |
. . . 4
⊢
∀𝑥 ∈
(0[,)+∞)∀𝑦
∈ (0[,)+∞)(𝑥
· 𝑦) ∈
(0[,)+∞) |
| 22 | | eqid 2737 |
. . . . . 6
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
| 23 | 22 | ringmgp 20236 |
. . . . 5
⊢
(ℂfld ∈ Ring →
(mulGrp‘ℂfld) ∈ Mnd) |
| 24 | | cnfldbas 21368 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
| 25 | 22, 24 | mgpbas 20142 |
. . . . . 6
⊢ ℂ =
(Base‘(mulGrp‘ℂfld)) |
| 26 | | cnfld1 21406 |
. . . . . . 7
⊢ 1 =
(1r‘ℂfld) |
| 27 | 22, 26 | ringidval 20180 |
. . . . . 6
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
| 28 | | cnfldmul 21372 |
. . . . . . 7
⊢ ·
= (.r‘ℂfld) |
| 29 | 22, 28 | mgpplusg 20141 |
. . . . . 6
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
| 30 | 25, 27, 29 | issubm 18816 |
. . . . 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 1342 |
. . 3
⊢
(0[,)+∞) ∈
(SubMnd‘(mulGrp‘ℂfld)) |
| 33 | | eqid 2737 |
. . . 4
⊢
((mulGrp‘ℂfld) ↾s
(0[,)+∞)) = ((mulGrp‘ℂfld) ↾s
(0[,)+∞)) |
| 34 | 33 | submmnd 18826 |
. . 3
⊢
((0[,)+∞) ∈
(SubMnd‘(mulGrp‘ℂfld)) →
((mulGrp‘ℂfld) ↾s (0[,)+∞))
∈ Mnd) |
| 35 | 32, 34 | ax-mp 5 |
. 2
⊢
((mulGrp‘ℂfld) ↾s
(0[,)+∞)) ∈ Mnd |
| 36 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑥
∈ (0[,)+∞)) |
| 37 | 10, 36 | sselid 3981 |
. . . . . . . 8
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑥
∈ ℂ) |
| 38 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑦
∈ (0[,)+∞)) |
| 39 | 10, 38 | sselid 3981 |
. . . . . . . 8
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑦
∈ ℂ) |
| 40 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑧
∈ (0[,)+∞)) |
| 41 | 10, 40 | sselid 3981 |
. . . . . . . 8
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → 𝑧
∈ ℂ) |
| 42 | 37, 39, 41 | adddid 11285 |
. . . . . . 7
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → (𝑥
· (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) |
| 43 | 37, 39, 41 | adddird 11286 |
. . . . . . 7
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → ((𝑥
+ 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
| 44 | 42, 43 | jca 511 |
. . . . . 6
⊢ (((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
∧ 𝑧 ∈
(0[,)+∞)) → ((𝑥
· (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) |
| 45 | 44 | ralrimiva 3146 |
. . . . 5
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ ∀𝑧 ∈
(0[,)+∞)((𝑥 ·
(𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) |
| 46 | 45 | ralrimiva 3146 |
. . . 4
⊢ (𝑥 ∈ (0[,)+∞) →
∀𝑦 ∈
(0[,)+∞)∀𝑧
∈ (0[,)+∞)((𝑥
· (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) |
| 47 | 10 | sseli 3979 |
. . . . 5
⊢ (𝑥 ∈ (0[,)+∞) →
𝑥 ∈
ℂ) |
| 48 | 47 | mul02d 11459 |
. . . 4
⊢ (𝑥 ∈ (0[,)+∞) → (0
· 𝑥) =
0) |
| 49 | 47 | mul01d 11460 |
. . . 4
⊢ (𝑥 ∈ (0[,)+∞) →
(𝑥 · 0) =
0) |
| 50 | 46, 48, 49 | jca32 515 |
. . 3
⊢ (𝑥 ∈ (0[,)+∞) →
(∀𝑦 ∈
(0[,)+∞)∀𝑧
∈ (0[,)+∞)((𝑥
· (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ ((0 · 𝑥) = 0 ∧ (𝑥 · 0) = 0))) |
| 51 | 50 | rgen 3063 |
. 2
⊢
∀𝑥 ∈
(0[,)+∞)(∀𝑦
∈ (0[,)+∞)∀𝑧 ∈ (0[,)+∞)((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ ((0 · 𝑥) = 0 ∧ (𝑥 · 0) = 0)) |
| 52 | 5, 24 | ressbas2 17283 |
. . . 4
⊢
((0[,)+∞) ⊆ ℂ → (0[,)+∞) =
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
| 53 | 10, 52 | ax-mp 5 |
. . 3
⊢
(0[,)+∞) = (Base‘(ℂfld ↾s
(0[,)+∞))) |
| 54 | | cnfldex 21367 |
. . . 4
⊢
ℂfld ∈ V |
| 55 | | ovex 7464 |
. . . 4
⊢
(0[,)+∞) ∈ V |
| 56 | 5, 22 | mgpress 20147 |
. . . 4
⊢
((ℂfld ∈ V ∧ (0[,)+∞) ∈ V) →
((mulGrp‘ℂfld) ↾s (0[,)+∞)) =
(mulGrp‘(ℂfld ↾s
(0[,)+∞)))) |
| 57 | 54, 55, 56 | mp2an 692 |
. . 3
⊢
((mulGrp‘ℂfld) ↾s
(0[,)+∞)) = (mulGrp‘(ℂfld ↾s
(0[,)+∞))) |
| 58 | | cnfldadd 21370 |
. . . . 5
⊢ + =
(+g‘ℂfld) |
| 59 | 5, 58 | ressplusg 17334 |
. . . 4
⊢
((0[,)+∞) ∈ V → + =
(+g‘(ℂfld ↾s
(0[,)+∞)))) |
| 60 | 55, 59 | ax-mp 5 |
. . 3
⊢ + =
(+g‘(ℂfld ↾s
(0[,)+∞))) |
| 61 | 5, 28 | ressmulr 17351 |
. . . 4
⊢
((0[,)+∞) ∈ V → · =
(.r‘(ℂfld ↾s
(0[,)+∞)))) |
| 62 | 55, 61 | ax-mp 5 |
. . 3
⊢ ·
= (.r‘(ℂfld ↾s
(0[,)+∞))) |
| 63 | | ringmnd 20240 |
. . . . 5
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
| 64 | 1, 63 | ax-mp 5 |
. . . 4
⊢
ℂfld ∈ Mnd |
| 65 | | 0e0icopnf 13498 |
. . . 4
⊢ 0 ∈
(0[,)+∞) |
| 66 | | cnfld0 21405 |
. . . . 5
⊢ 0 =
(0g‘ℂfld) |
| 67 | 5, 24, 66 | ress0g 18775 |
. . . 4
⊢
((ℂfld ∈ Mnd ∧ 0 ∈ (0[,)+∞) ∧
(0[,)+∞) ⊆ ℂ) → 0 =
(0g‘(ℂfld ↾s
(0[,)+∞)))) |
| 68 | 64, 65, 10, 67 | mp3an 1463 |
. . 3
⊢ 0 =
(0g‘(ℂfld ↾s
(0[,)+∞))) |
| 69 | 53, 57, 60, 62, 68 | issrg 20185 |
. 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 1342 |
1
⊢
(ℂfld ↾s (0[,)+∞)) ∈
SRing |