| Step | Hyp | Ref
| Expression |
| 1 | | ccfldextrr 33699 |
. . 3
⊢
ℂfld/FldExtℝfld |
| 2 | | extdgval 33705 |
. . 3
⊢
(ℂfld/FldExtℝfld →
(ℂfld[:]ℝfld) = (dim‘((subringAlg
‘ℂfld)‘(Base‘ℝfld)))) |
| 3 | 1, 2 | ax-mp 5 |
. 2
⊢
(ℂfld[:]ℝfld) =
(dim‘((subringAlg
‘ℂfld)‘(Base‘ℝfld))) |
| 4 | | rebase 21624 |
. . . 4
⊢ ℝ =
(Base‘ℝfld) |
| 5 | 4 | fveq2i 6909 |
. . 3
⊢
((subringAlg ‘ℂfld)‘ℝ) = ((subringAlg
‘ℂfld)‘(Base‘ℝfld)) |
| 6 | 5 | fveq2i 6909 |
. 2
⊢
(dim‘((subringAlg ‘ℂfld)‘ℝ)) =
(dim‘((subringAlg
‘ℂfld)‘(Base‘ℝfld))) |
| 7 | | ccfldsrarelvec 33721 |
. . . 4
⊢
((subringAlg ‘ℂfld)‘ℝ) ∈
LVec |
| 8 | | df-pr 4629 |
. . . . . 6
⊢ {1, i} =
({1} ∪ {i}) |
| 9 | | eqid 2737 |
. . . . . . . 8
⊢
(LSpan‘((subringAlg ‘ℂfld)‘ℝ))
= (LSpan‘((subringAlg
‘ℂfld)‘ℝ)) |
| 10 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (⊤
→ ((subringAlg ‘ℂfld)‘ℝ) = ((subringAlg
‘ℂfld)‘ℝ)) |
| 11 | | cnfld0 21405 |
. . . . . . . . . . 11
⊢ 0 =
(0g‘ℂfld) |
| 12 | 11 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ 0 = (0g‘ℂfld)) |
| 13 | | ax-resscn 11212 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
| 14 | | cnfldbas 21368 |
. . . . . . . . . . . 12
⊢ ℂ =
(Base‘ℂfld) |
| 15 | 13, 14 | sseqtri 4032 |
. . . . . . . . . . 11
⊢ ℝ
⊆ (Base‘ℂfld) |
| 16 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ℝ ⊆ (Base‘ℂfld)) |
| 17 | 10, 12, 16 | sralmod0 21195 |
. . . . . . . . 9
⊢ (⊤
→ 0 = (0g‘((subringAlg
‘ℂfld)‘ℝ))) |
| 18 | 17 | mptru 1547 |
. . . . . . . 8
⊢ 0 =
(0g‘((subringAlg
‘ℂfld)‘ℝ)) |
| 19 | 7 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ ((subringAlg ‘ℂfld)‘ℝ) ∈
LVec) |
| 20 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 21 | | ax-1ne0 11224 |
. . . . . . . . . 10
⊢ 1 ≠
0 |
| 22 | 10, 16 | srabase 21177 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (Base‘ℂfld) = (Base‘((subringAlg
‘ℂfld)‘ℝ))) |
| 23 | 22 | mptru 1547 |
. . . . . . . . . . . 12
⊢
(Base‘ℂfld) = (Base‘((subringAlg
‘ℂfld)‘ℝ)) |
| 24 | 14, 23 | eqtri 2765 |
. . . . . . . . . . 11
⊢ ℂ =
(Base‘((subringAlg
‘ℂfld)‘ℝ)) |
| 25 | 24, 18 | lindssn 33406 |
. . . . . . . . . 10
⊢
((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec
∧ 1 ∈ ℂ ∧ 1 ≠ 0) → {1} ∈
(LIndS‘((subringAlg
‘ℂfld)‘ℝ))) |
| 26 | 7, 20, 21, 25 | mp3an 1463 |
. . . . . . . . 9
⊢ {1}
∈ (LIndS‘((subringAlg
‘ℂfld)‘ℝ)) |
| 27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ {1} ∈ (LIndS‘((subringAlg
‘ℂfld)‘ℝ))) |
| 28 | | ax-icn 11214 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
| 29 | | ine0 11698 |
. . . . . . . . . 10
⊢ i ≠
0 |
| 30 | 24, 18 | lindssn 33406 |
. . . . . . . . . 10
⊢
((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec
∧ i ∈ ℂ ∧ i ≠ 0) → {i} ∈
(LIndS‘((subringAlg
‘ℂfld)‘ℝ))) |
| 31 | 7, 28, 29, 30 | mp3an 1463 |
. . . . . . . . 9
⊢ {i}
∈ (LIndS‘((subringAlg
‘ℂfld)‘ℝ)) |
| 32 | 31 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ {i} ∈ (LIndS‘((subringAlg
‘ℂfld)‘ℝ))) |
| 33 | | lveclmod 21105 |
. . . . . . . . . . . . . . 15
⊢
(((subringAlg ‘ℂfld)‘ℝ) ∈ LVec
→ ((subringAlg ‘ℂfld)‘ℝ) ∈
LMod) |
| 34 | 7, 33 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((subringAlg ‘ℂfld)‘ℝ) ∈
LMod |
| 35 | | df-refld 21623 |
. . . . . . . . . . . . . . . 16
⊢
ℝfld = (ℂfld ↾s
ℝ) |
| 36 | 10, 16 | srasca 21183 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ (ℂfld ↾s ℝ) =
(Scalar‘((subringAlg
‘ℂfld)‘ℝ))) |
| 37 | 36 | mptru 1547 |
. . . . . . . . . . . . . . . 16
⊢
(ℂfld ↾s ℝ) =
(Scalar‘((subringAlg
‘ℂfld)‘ℝ)) |
| 38 | 35, 37 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢
ℝfld = (Scalar‘((subringAlg
‘ℂfld)‘ℝ)) |
| 39 | | cnfldmul 21372 |
. . . . . . . . . . . . . . . 16
⊢ ·
= (.r‘ℂfld) |
| 40 | 10, 16 | sravsca 21185 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ (.r‘ℂfld) = (
·𝑠 ‘((subringAlg
‘ℂfld)‘ℝ))) |
| 41 | 40 | mptru 1547 |
. . . . . . . . . . . . . . . 16
⊢
(.r‘ℂfld) = (
·𝑠 ‘((subringAlg
‘ℂfld)‘ℝ)) |
| 42 | 39, 41 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ ·
= ( ·𝑠 ‘((subringAlg
‘ℂfld)‘ℝ)) |
| 43 | 38, 4, 24, 42, 9 | ellspsn 21001 |
. . . . . . . . . . . . . 14
⊢
((((subringAlg ‘ℂfld)‘ℝ) ∈ LMod
∧ 1 ∈ ℂ) → (𝑧 ∈ ((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1}) ↔ ∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1))) |
| 44 | 34, 20, 43 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1}) ↔ ∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1)) |
| 45 | 38, 4, 24, 42, 9 | ellspsn 21001 |
. . . . . . . . . . . . . 14
⊢
((((subringAlg ‘ℂfld)‘ℝ) ∈ LMod
∧ i ∈ ℂ) → (𝑧 ∈ ((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{i}) ↔ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i))) |
| 46 | 34, 28, 45 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{i}) ↔ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)) |
| 47 | 44, 46 | anbi12i 628 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{i})) ↔ (∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1) ∧ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i))) |
| 48 | | reeanv 3229 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1) ∧ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i))) |
| 49 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑥 · 1)) |
| 50 | | simpll 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℝ) |
| 51 | 50 | recnd 11289 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℂ) |
| 52 | 51 | mulridd 11278 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑥 · 1) = 𝑥) |
| 53 | 49, 52 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 𝑥) |
| 54 | 53 | negeqd 11502 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑧 = -𝑥) |
| 55 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑦 · i)) |
| 56 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℝ) |
| 57 | 56 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℂ) |
| 58 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → i ∈
ℂ) |
| 59 | 57, 58 | mulcomd 11282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑦 · i) = (i · 𝑦)) |
| 60 | 55, 59 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (i · 𝑦)) |
| 61 | 54, 60 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = (-𝑥 + (i · 𝑦))) |
| 62 | 53, 51 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 ∈ ℂ) |
| 63 | 62 | subidd 11608 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑧 − 𝑧) = 0) |
| 64 | 63 | negeqd 11502 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧 − 𝑧) = -0) |
| 65 | 62, 62 | negsubdid 11635 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧 − 𝑧) = (-𝑧 + 𝑧)) |
| 66 | | neg0 11555 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ -0 =
0 |
| 67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 =
0) |
| 68 | 64, 65, 67 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = 0) |
| 69 | 61, 68 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑥 + (i · 𝑦)) = 0) |
| 70 | 50 | renegcld 11690 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑥 ∈ ℝ) |
| 71 | | creq0 32746 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((-𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((-𝑥 = 0 ∧ 𝑦 = 0) ↔ (-𝑥 + (i · 𝑦)) = 0)) |
| 72 | 70, 56, 71 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → ((-𝑥 = 0 ∧ 𝑦 = 0) ↔ (-𝑥 + (i · 𝑦)) = 0)) |
| 73 | 69, 72 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑥 = 0 ∧ 𝑦 = 0)) |
| 74 | 73 | simpld 494 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑥 = 0) |
| 75 | 51, 74 | negcon1ad 11615 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 = 𝑥) |
| 76 | 53, 75, 67 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 0) |
| 77 | 76 | ex 412 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0)) |
| 78 | 77 | rexlimivv 3201 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0) |
| 79 | | 0red 11264 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 0 → 0 ∈
ℝ) |
| 80 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 = 0 ∧ 𝑥 = 0) → 𝑥 = 0) |
| 81 | 80 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑥 · 1) = (0 ·
1)) |
| 82 | 81 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑧 = (𝑥 · 1) ↔ 𝑧 = (0 · 1))) |
| 83 | 82 | anbi1d 631 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 = 0 ∧ 𝑥 = 0) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)))) |
| 84 | 83 | rexbidv 3179 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 0 ∧ 𝑥 = 0) → (∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)))) |
| 85 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 = 0 ∧ 𝑦 = 0) → 𝑦 = 0) |
| 86 | 85 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑦 · i) = (0 ·
i)) |
| 87 | 86 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑧 = (𝑦 · i) ↔ 𝑧 = (0 · i))) |
| 88 | 87 | anbi2d 630 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 = 0 ∧ 𝑦 = 0) → ((𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i)))) |
| 89 | 20 | mul02i 11450 |
. . . . . . . . . . . . . . . . . 18
⊢ (0
· 1) = 0 |
| 90 | 89 | eqeq2i 2750 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (0 · 1) ↔ 𝑧 = 0) |
| 91 | 90 | biimpri 228 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 0 → 𝑧 = (0 · 1)) |
| 92 | 28 | mul02i 11450 |
. . . . . . . . . . . . . . . . . 18
⊢ (0
· i) = 0 |
| 93 | 92 | eqeq2i 2750 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (0 · i) ↔ 𝑧 = 0) |
| 94 | 93 | biimpri 228 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 0 → 𝑧 = (0 · i)) |
| 95 | 91, 94 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 0 → (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i))) |
| 96 | 79, 88, 95 | rspcedvd 3624 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 0 → ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i))) |
| 97 | 79, 84, 96 | rspcedvd 3624 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 0 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) |
| 98 | 78, 97 | impbii 209 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ 𝑧 = 0) |
| 99 | 47, 48, 98 | 3bitr2i 299 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{i})) ↔ 𝑧 = 0) |
| 100 | | elin 3967 |
. . . . . . . . . . 11
⊢ (𝑧 ∈
(((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1}) ∩
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{i})) ↔ (𝑧 ∈
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{i}))) |
| 101 | | velsn 4642 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {0} ↔ 𝑧 = 0) |
| 102 | 99, 100, 101 | 3bitr4i 303 |
. . . . . . . . . 10
⊢ (𝑧 ∈
(((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1}) ∩
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{i})) ↔ 𝑧 ∈ {0}) |
| 103 | 102 | eqriv 2734 |
. . . . . . . . 9
⊢
(((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1}) ∩
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{i})) =
{0} |
| 104 | 103 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1}) ∩
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{i})) =
{0}) |
| 105 | 9, 18, 19, 27, 32, 104 | lindsun 33676 |
. . . . . . 7
⊢ (⊤
→ ({1} ∪ {i}) ∈ (LIndS‘((subringAlg
‘ℂfld)‘ℝ))) |
| 106 | 105 | mptru 1547 |
. . . . . 6
⊢ ({1}
∪ {i}) ∈ (LIndS‘((subringAlg
‘ℂfld)‘ℝ)) |
| 107 | 8, 106 | eqeltri 2837 |
. . . . 5
⊢ {1, i}
∈ (LIndS‘((subringAlg
‘ℂfld)‘ℝ)) |
| 108 | | cnfldadd 21370 |
. . . . . . . . . 10
⊢ + =
(+g‘ℂfld) |
| 109 | 10, 16 | sraaddg 21179 |
. . . . . . . . . . 11
⊢ (⊤
→ (+g‘ℂfld) =
(+g‘((subringAlg
‘ℂfld)‘ℝ))) |
| 110 | 109 | mptru 1547 |
. . . . . . . . . 10
⊢
(+g‘ℂfld) =
(+g‘((subringAlg
‘ℂfld)‘ℝ)) |
| 111 | 108, 110 | eqtri 2765 |
. . . . . . . . 9
⊢ + =
(+g‘((subringAlg
‘ℂfld)‘ℝ)) |
| 112 | 34 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ ((subringAlg ‘ℂfld)‘ℝ) ∈
LMod) |
| 113 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (⊤
→ 1 ∈ ℂ) |
| 114 | 28 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ i ∈ ℂ) |
| 115 | 24, 111, 38, 4, 42, 9, 112, 113, 114 | lspprel 21093 |
. . . . . . . 8
⊢ (⊤
→ (𝑧 ∈
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)))) |
| 116 | 115 | mptru 1547 |
. . . . . . 7
⊢ (𝑧 ∈
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i))) |
| 117 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈
ℝ) |
| 118 | 117 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈
ℂ) |
| 119 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) |
| 120 | 118, 119 | mulcld 11281 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 1) ∈
ℂ) |
| 121 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℝ) |
| 122 | 121 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℂ) |
| 123 | 28 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → i ∈
ℂ) |
| 124 | 122, 123 | mulcld 11281 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · i) ∈
ℂ) |
| 125 | 120, 124 | addcld 11280 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + (𝑦 · i)) ∈
ℂ) |
| 126 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → (𝑧 ∈ ℂ ↔ ((𝑥 · 1) + (𝑦 · i)) ∈
ℂ)) |
| 127 | 125, 126 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈ ℂ)) |
| 128 | 127 | rexlimivv 3201 |
. . . . . . . 8
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈
ℂ) |
| 129 | | recl 15149 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℂ →
(ℜ‘𝑧) ∈
ℝ) |
| 130 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → 𝑥 = (ℜ‘𝑧)) |
| 131 | 130 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑥 · 1) = ((ℜ‘𝑧) · 1)) |
| 132 | 131 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → ((𝑥 · 1) + (𝑦 · i)) = (((ℜ‘𝑧) · 1) + (𝑦 · i))) |
| 133 | 132 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)))) |
| 134 | 133 | rexbidv 3179 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)))) |
| 135 | | imcl 15150 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℂ →
(ℑ‘𝑧) ∈
ℝ) |
| 136 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → 𝑦 = (ℑ‘𝑧)) |
| 137 | 136 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑦 · i) = ((ℑ‘𝑧) · i)) |
| 138 | 137 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (((ℜ‘𝑧) · 1) + (𝑦 · i)) =
(((ℜ‘𝑧) ·
1) + ((ℑ‘𝑧)
· i))) |
| 139 | 138 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) ·
i)))) |
| 140 | | replim 15155 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℂ → 𝑧 = ((ℜ‘𝑧) + (i ·
(ℑ‘𝑧)))) |
| 141 | 129 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℂ →
(ℜ‘𝑧) ∈
ℂ) |
| 142 | 141 | mulridd 11278 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℂ →
((ℜ‘𝑧) ·
1) = (ℜ‘𝑧)) |
| 143 | 135 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℂ →
(ℑ‘𝑧) ∈
ℂ) |
| 144 | 28 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℂ → i ∈
ℂ) |
| 145 | 143, 144 | mulcomd 11282 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℂ →
((ℑ‘𝑧) ·
i) = (i · (ℑ‘𝑧))) |
| 146 | 142, 145 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℂ →
(((ℜ‘𝑧) ·
1) + ((ℑ‘𝑧)
· i)) = ((ℜ‘𝑧) + (i · (ℑ‘𝑧)))) |
| 147 | 140, 146 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℂ → 𝑧 = (((ℜ‘𝑧) · 1) +
((ℑ‘𝑧) ·
i))) |
| 148 | 135, 139,
147 | rspcedvd 3624 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℂ →
∃𝑦 ∈ ℝ
𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i))) |
| 149 | 129, 134,
148 | rspcedvd 3624 |
. . . . . . . 8
⊢ (𝑧 ∈ ℂ →
∃𝑥 ∈ ℝ
∃𝑦 ∈ ℝ
𝑧 = ((𝑥 · 1) + (𝑦 · i))) |
| 150 | 128, 149 | impbii 209 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 ∈
ℂ) |
| 151 | 116, 150 | bitri 275 |
. . . . . 6
⊢ (𝑧 ∈
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1, i}) ↔ 𝑧 ∈
ℂ) |
| 152 | 151 | eqriv 2734 |
. . . . 5
⊢
((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1, i}) =
ℂ |
| 153 | | eqid 2737 |
. . . . . 6
⊢
(LBasis‘((subringAlg ‘ℂfld)‘ℝ))
= (LBasis‘((subringAlg
‘ℂfld)‘ℝ)) |
| 154 | 24, 153, 9 | islbs4 21852 |
. . . . 5
⊢ ({1, i}
∈ (LBasis‘((subringAlg ‘ℂfld)‘ℝ))
↔ ({1, i} ∈ (LIndS‘((subringAlg
‘ℂfld)‘ℝ)) ∧ ((LSpan‘((subringAlg
‘ℂfld)‘ℝ))‘{1, i}) =
ℂ)) |
| 155 | 107, 152,
154 | mpbir2an 711 |
. . . 4
⊢ {1, i}
∈ (LBasis‘((subringAlg
‘ℂfld)‘ℝ)) |
| 156 | 153 | dimval 33651 |
. . . 4
⊢
((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec
∧ {1, i} ∈ (LBasis‘((subringAlg
‘ℂfld)‘ℝ))) → (dim‘((subringAlg
‘ℂfld)‘ℝ)) = (♯‘{1,
i})) |
| 157 | 7, 155, 156 | mp2an 692 |
. . 3
⊢
(dim‘((subringAlg ‘ℂfld)‘ℝ)) =
(♯‘{1, i}) |
| 158 | | 1nei 32747 |
. . . 4
⊢ 1 ≠
i |
| 159 | | hashprg 14434 |
. . . . 5
⊢ ((1
∈ ℂ ∧ i ∈ ℂ) → (1 ≠ i ↔
(♯‘{1, i}) = 2)) |
| 160 | 20, 28, 159 | mp2an 692 |
. . . 4
⊢ (1 ≠ i
↔ (♯‘{1, i}) = 2) |
| 161 | 158, 160 | mpbi 230 |
. . 3
⊢
(♯‘{1, i}) = 2 |
| 162 | 157, 161 | eqtri 2765 |
. 2
⊢
(dim‘((subringAlg ‘ℂfld)‘ℝ)) =
2 |
| 163 | 3, 6, 162 | 3eqtr2i 2771 |
1
⊢
(ℂfld[:]ℝfld) = 2 |