| 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 | | nn0subm 21440 |
. . 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 | | nn0ex 12532 |
. . . 4
⊢
ℕ0 ∈ V |
| 9 | | eqid 2737 |
. . . . 5
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
| 10 | 5, 9 | mgpress 20147 |
. . . 4
⊢
((ℂfld ∈ CMnd ∧ ℕ0 ∈ V)
→ ((mulGrp‘ℂfld) ↾s
ℕ0) = (mulGrp‘(ℂfld ↾s
ℕ0))) |
| 11 | 3, 8, 10 | mp2an 692 |
. . 3
⊢
((mulGrp‘ℂfld) ↾s
ℕ0) = (mulGrp‘(ℂfld ↾s
ℕ0)) |
| 12 | | nn0sscn 12531 |
. . . . 5
⊢
ℕ0 ⊆ ℂ |
| 13 | | 1nn0 12542 |
. . . . 5
⊢ 1 ∈
ℕ0 |
| 14 | | nn0mulcl 12562 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑥 · 𝑦) ∈
ℕ0) |
| 15 | 14 | rgen2 3199 |
. . . . 5
⊢
∀𝑥 ∈
ℕ0 ∀𝑦 ∈ ℕ0 (𝑥 · 𝑦) ∈ ℕ0 |
| 16 | 9 | ringmgp 20236 |
. . . . . . 7
⊢
(ℂfld ∈ Ring →
(mulGrp‘ℂfld) ∈ Mnd) |
| 17 | 1, 16 | ax-mp 5 |
. . . . . 6
⊢
(mulGrp‘ℂfld) ∈ Mnd |
| 18 | | cnfldbas 21368 |
. . . . . . . 8
⊢ ℂ =
(Base‘ℂfld) |
| 19 | 9, 18 | mgpbas 20142 |
. . . . . . 7
⊢ ℂ =
(Base‘(mulGrp‘ℂfld)) |
| 20 | | cnfld1 21406 |
. . . . . . . 8
⊢ 1 =
(1r‘ℂfld) |
| 21 | 9, 20 | ringidval 20180 |
. . . . . . 7
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
| 22 | | cnfldmul 21372 |
. . . . . . . 8
⊢ ·
= (.r‘ℂfld) |
| 23 | 9, 22 | mgpplusg 20141 |
. . . . . . 7
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
| 24 | 19, 21, 23 | issubm 18816 |
. . . . . 6
⊢
((mulGrp‘ℂfld) ∈ Mnd →
(ℕ0 ∈ (SubMnd‘(mulGrp‘ℂfld))
↔ (ℕ0 ⊆ ℂ ∧ 1 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 ∀𝑦 ∈ ℕ0 (𝑥 · 𝑦) ∈
ℕ0))) |
| 25 | 17, 24 | ax-mp 5 |
. . . . 5
⊢
(ℕ0 ∈
(SubMnd‘(mulGrp‘ℂfld)) ↔ (ℕ0
⊆ ℂ ∧ 1 ∈ ℕ0 ∧ ∀𝑥 ∈ ℕ0
∀𝑦 ∈
ℕ0 (𝑥
· 𝑦) ∈
ℕ0)) |
| 26 | 12, 13, 15, 25 | mpbir3an 1342 |
. . . 4
⊢
ℕ0 ∈
(SubMnd‘(mulGrp‘ℂfld)) |
| 27 | | eqid 2737 |
. . . . 5
⊢
((mulGrp‘ℂfld) ↾s
ℕ0) = ((mulGrp‘ℂfld)
↾s ℕ0) |
| 28 | 27 | submmnd 18826 |
. . . 4
⊢
(ℕ0 ∈
(SubMnd‘(mulGrp‘ℂfld)) →
((mulGrp‘ℂfld) ↾s ℕ0)
∈ Mnd) |
| 29 | 26, 28 | ax-mp 5 |
. . 3
⊢
((mulGrp‘ℂfld) ↾s
ℕ0) ∈ Mnd |
| 30 | 11, 29 | eqeltrri 2838 |
. 2
⊢
(mulGrp‘(ℂfld ↾s
ℕ0)) ∈ Mnd |
| 31 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ0
∧ (𝑦 ∈
ℕ0 ∧ 𝑧
∈ ℕ0)) → 𝑥 ∈ ℕ0) |
| 32 | 31 | nn0cnd 12589 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ (𝑦 ∈
ℕ0 ∧ 𝑧
∈ ℕ0)) → 𝑥 ∈ ℂ) |
| 33 | | simprl 771 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ0
∧ (𝑦 ∈
ℕ0 ∧ 𝑧
∈ ℕ0)) → 𝑦 ∈ ℕ0) |
| 34 | 33 | nn0cnd 12589 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ (𝑦 ∈
ℕ0 ∧ 𝑧
∈ ℕ0)) → 𝑦 ∈ ℂ) |
| 35 | | simprr 773 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ0
∧ (𝑦 ∈
ℕ0 ∧ 𝑧
∈ ℕ0)) → 𝑧 ∈ ℕ0) |
| 36 | 35 | nn0cnd 12589 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ (𝑦 ∈
ℕ0 ∧ 𝑧
∈ ℕ0)) → 𝑧 ∈ ℂ) |
| 37 | 32, 34, 36 | adddid 11285 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ0
∧ (𝑦 ∈
ℕ0 ∧ 𝑧
∈ ℕ0)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) |
| 38 | 32, 34, 36 | adddird 11286 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ0
∧ (𝑦 ∈
ℕ0 ∧ 𝑧
∈ ℕ0)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
| 39 | 37, 38 | jca 511 |
. . . . 5
⊢ ((𝑥 ∈ ℕ0
∧ (𝑦 ∈
ℕ0 ∧ 𝑧
∈ ℕ0)) → ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) |
| 40 | 39 | ralrimivva 3202 |
. . . 4
⊢ (𝑥 ∈ ℕ0
→ ∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)))) |
| 41 | | nn0cn 12536 |
. . . . 5
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℂ) |
| 42 | 41 | mul02d 11459 |
. . . 4
⊢ (𝑥 ∈ ℕ0
→ (0 · 𝑥) =
0) |
| 43 | 41 | mul01d 11460 |
. . . 4
⊢ (𝑥 ∈ ℕ0
→ (𝑥 · 0) =
0) |
| 44 | 40, 42, 43 | jca32 515 |
. . 3
⊢ (𝑥 ∈ ℕ0
→ (∀𝑦 ∈
ℕ0 ∀𝑧 ∈ ℕ0 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ ((0 · 𝑥) = 0 ∧ (𝑥 · 0) = 0))) |
| 45 | 44 | rgen 3063 |
. 2
⊢
∀𝑥 ∈
ℕ0 (∀𝑦 ∈ ℕ0 ∀𝑧 ∈ ℕ0
((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ ((0 · 𝑥) = 0 ∧ (𝑥 · 0) = 0)) |
| 46 | 5, 18 | ressbas2 17283 |
. . . 4
⊢
(ℕ0 ⊆ ℂ → ℕ0 =
(Base‘(ℂfld ↾s
ℕ0))) |
| 47 | 12, 46 | ax-mp 5 |
. . 3
⊢
ℕ0 = (Base‘(ℂfld
↾s ℕ0)) |
| 48 | | eqid 2737 |
. . 3
⊢
(mulGrp‘(ℂfld ↾s
ℕ0)) = (mulGrp‘(ℂfld
↾s ℕ0)) |
| 49 | | cnfldadd 21370 |
. . . . 5
⊢ + =
(+g‘ℂfld) |
| 50 | 5, 49 | ressplusg 17334 |
. . . 4
⊢
(ℕ0 ∈ V → + =
(+g‘(ℂfld ↾s
ℕ0))) |
| 51 | 8, 50 | ax-mp 5 |
. . 3
⊢ + =
(+g‘(ℂfld ↾s
ℕ0)) |
| 52 | 5, 22 | ressmulr 17351 |
. . . 4
⊢
(ℕ0 ∈ V → · =
(.r‘(ℂfld ↾s
ℕ0))) |
| 53 | 8, 52 | ax-mp 5 |
. . 3
⊢ ·
= (.r‘(ℂfld ↾s
ℕ0)) |
| 54 | | ringmnd 20240 |
. . . . 5
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
| 55 | 1, 54 | ax-mp 5 |
. . . 4
⊢
ℂfld ∈ Mnd |
| 56 | | 0nn0 12541 |
. . . 4
⊢ 0 ∈
ℕ0 |
| 57 | | cnfld0 21405 |
. . . . 5
⊢ 0 =
(0g‘ℂfld) |
| 58 | 5, 18, 57 | ress0g 18775 |
. . . 4
⊢
((ℂfld ∈ Mnd ∧ 0 ∈ ℕ0
∧ ℕ0 ⊆ ℂ) → 0 =
(0g‘(ℂfld ↾s
ℕ0))) |
| 59 | 55, 56, 12, 58 | mp3an 1463 |
. . 3
⊢ 0 =
(0g‘(ℂfld ↾s
ℕ0)) |
| 60 | 47, 48, 51, 53, 59 | issrg 20185 |
. 2
⊢
((ℂfld ↾s ℕ0) ∈
SRing ↔ ((ℂfld ↾s ℕ0)
∈ CMnd ∧ (mulGrp‘(ℂfld ↾s
ℕ0)) ∈ Mnd ∧ ∀𝑥 ∈ ℕ0 (∀𝑦 ∈ ℕ0
∀𝑧 ∈
ℕ0 ((𝑥
· (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ ((0 · 𝑥) = 0 ∧ (𝑥 · 0) = 0)))) |
| 61 | 7, 30, 45, 60 | mpbir3an 1342 |
1
⊢
(ℂfld ↾s ℕ0) ∈
SRing |