Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ccfldextdgrr Structured version   Visualization version   GIF version

Theorem ccfldextdgrr 32584
Description: The degree of the field extension of the complex numbers over the real numbers is 2. (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 20-Aug-2023.)
Assertion
Ref Expression
ccfldextdgrr (ℂfld[:]ℝfld) = 2

Proof of Theorem ccfldextdgrr
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ccfldextrr 32565 . . 3 fld/FldExtfld
2 extdgval 32571 . . 3 (ℂfld/FldExtfld → (ℂfld[:]ℝfld) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld))))
31, 2ax-mp 5 . 2 (ℂfld[:]ℝfld) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld)))
4 rebase 21092 . . . 4 ℝ = (Base‘ℝfld)
54fveq2i 6881 . . 3 ((subringAlg ‘ℂfld)‘ℝ) = ((subringAlg ‘ℂfld)‘(Base‘ℝfld))
65fveq2i 6881 . 2 (dim‘((subringAlg ‘ℂfld)‘ℝ)) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld)))
7 ccfldsrarelvec 32583 . . . 4 ((subringAlg ‘ℂfld)‘ℝ) ∈ LVec
8 df-pr 4625 . . . . . 6 {1, i} = ({1} ∪ {i})
9 eqid 2731 . . . . . . . 8 (LSpan‘((subringAlg ‘ℂfld)‘ℝ)) = (LSpan‘((subringAlg ‘ℂfld)‘ℝ))
10 eqidd 2732 . . . . . . . . . 10 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) = ((subringAlg ‘ℂfld)‘ℝ))
11 cnfld0 20903 . . . . . . . . . . 11 0 = (0g‘ℂfld)
1211a1i 11 . . . . . . . . . 10 (⊤ → 0 = (0g‘ℂfld))
13 ax-resscn 11149 . . . . . . . . . . . 12 ℝ ⊆ ℂ
14 cnfldbas 20882 . . . . . . . . . . . 12 ℂ = (Base‘ℂfld)
1513, 14sseqtri 4014 . . . . . . . . . . 11 ℝ ⊆ (Base‘ℂfld)
1615a1i 11 . . . . . . . . . 10 (⊤ → ℝ ⊆ (Base‘ℂfld))
1710, 12, 16sralmod0 20758 . . . . . . . . 9 (⊤ → 0 = (0g‘((subringAlg ‘ℂfld)‘ℝ)))
1817mptru 1548 . . . . . . . 8 0 = (0g‘((subringAlg ‘ℂfld)‘ℝ))
197a1i 11 . . . . . . . 8 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) ∈ LVec)
20 ax-1cn 11150 . . . . . . . . . 10 1 ∈ ℂ
21 ax-1ne0 11161 . . . . . . . . . 10 1 ≠ 0
2210, 16srabase 20741 . . . . . . . . . . . . 13 (⊤ → (Base‘ℂfld) = (Base‘((subringAlg ‘ℂfld)‘ℝ)))
2322mptru 1548 . . . . . . . . . . . 12 (Base‘ℂfld) = (Base‘((subringAlg ‘ℂfld)‘ℝ))
2414, 23eqtri 2759 . . . . . . . . . . 11 ℂ = (Base‘((subringAlg ‘ℂfld)‘ℝ))
2524, 18lindssn 32352 . . . . . . . . . 10 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → {1} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
267, 20, 21, 25mp3an 1461 . . . . . . . . 9 {1} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
2726a1i 11 . . . . . . . 8 (⊤ → {1} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
28 ax-icn 11151 . . . . . . . . . 10 i ∈ ℂ
29 ine0 11631 . . . . . . . . . 10 i ≠ 0
3024, 18lindssn 32352 . . . . . . . . . 10 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec ∧ i ∈ ℂ ∧ i ≠ 0) → {i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
317, 28, 29, 30mp3an 1461 . . . . . . . . 9 {i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
3231a1i 11 . . . . . . . 8 (⊤ → {i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
33 lveclmod 20666 . . . . . . . . . . . . . . 15 (((subringAlg ‘ℂfld)‘ℝ) ∈ LVec → ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod)
347, 33ax-mp 5 . . . . . . . . . . . . . 14 ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod
35 df-refld 21091 . . . . . . . . . . . . . . . 16 fld = (ℂflds ℝ)
3610, 16srasca 20747 . . . . . . . . . . . . . . . . 17 (⊤ → (ℂflds ℝ) = (Scalar‘((subringAlg ‘ℂfld)‘ℝ)))
3736mptru 1548 . . . . . . . . . . . . . . . 16 (ℂflds ℝ) = (Scalar‘((subringAlg ‘ℂfld)‘ℝ))
3835, 37eqtri 2759 . . . . . . . . . . . . . . 15 fld = (Scalar‘((subringAlg ‘ℂfld)‘ℝ))
39 cnfldmul 20884 . . . . . . . . . . . . . . . 16 · = (.r‘ℂfld)
4010, 16sravsca 20749 . . . . . . . . . . . . . . . . 17 (⊤ → (.r‘ℂfld) = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ)))
4140mptru 1548 . . . . . . . . . . . . . . . 16 (.r‘ℂfld) = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ))
4239, 41eqtri 2759 . . . . . . . . . . . . . . 15 · = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ))
4338, 4, 24, 42, 9lspsnel 20563 . . . . . . . . . . . . . 14 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LMod ∧ 1 ∈ ℂ) → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ↔ ∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1)))
4434, 20, 43mp2an 690 . . . . . . . . . . . . 13 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ↔ ∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1))
4538, 4, 24, 42, 9lspsnel 20563 . . . . . . . . . . . . . 14 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LMod ∧ i ∈ ℂ) → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i}) ↔ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
4634, 28, 45mp2an 690 . . . . . . . . . . . . 13 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i}) ↔ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i))
4744, 46anbi12i 627 . . . . . . . . . . . 12 ((𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ (∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1) ∧ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
48 reeanv 3225 . . . . . . . . . . . 12 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1) ∧ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
49 simprl 769 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑥 · 1))
50 simpll 765 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℝ)
5150recnd 11224 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℂ)
5251mulridd 11213 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑥 · 1) = 𝑥)
5349, 52eqtrd 2771 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 𝑥)
5453negeqd 11436 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑧 = -𝑥)
55 simprr 771 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑦 · i))
56 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℝ)
5756recnd 11224 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℂ)
5828a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → i ∈ ℂ)
5957, 58mulcomd 11217 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑦 · i) = (i · 𝑦))
6055, 59eqtrd 2771 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (i · 𝑦))
6154, 60oveq12d 7411 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = (-𝑥 + (i · 𝑦)))
6253, 51eqeltrd 2832 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 ∈ ℂ)
6362subidd 11541 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑧𝑧) = 0)
6463negeqd 11436 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧𝑧) = -0)
6562, 62negsubdid 11568 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧𝑧) = (-𝑧 + 𝑧))
66 neg0 11488 . . . . . . . . . . . . . . . . . . . . . 22 -0 = 0
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 = 0)
6864, 65, 673eqtr3d 2779 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = 0)
6961, 68eqtr3d 2773 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑥 + (i · 𝑦)) = 0)
7050renegcld 11623 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑥 ∈ ℝ)
71 creq0 31831 . . . . . . . . . . . . . . . . . . . 20 ((-𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((-𝑥 = 0 ∧ 𝑦 = 0) ↔ (-𝑥 + (i · 𝑦)) = 0))
7270, 56, 71syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → ((-𝑥 = 0 ∧ 𝑦 = 0) ↔ (-𝑥 + (i · 𝑦)) = 0))
7369, 72mpbird 256 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑥 = 0 ∧ 𝑦 = 0))
7473simpld 495 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑥 = 0)
7551, 74negcon1ad 11548 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 = 𝑥)
7653, 75, 673eqtr2d 2777 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 0)
7776ex 413 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0))
7877rexlimivv 3198 . . . . . . . . . . . . 13 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0)
79 0red 11199 . . . . . . . . . . . . . 14 (𝑧 = 0 → 0 ∈ ℝ)
80 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 0 ∧ 𝑥 = 0) → 𝑥 = 0)
8180oveq1d 7408 . . . . . . . . . . . . . . . . 17 ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑥 · 1) = (0 · 1))
8281eqeq2d 2742 . . . . . . . . . . . . . . . 16 ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑧 = (𝑥 · 1) ↔ 𝑧 = (0 · 1)))
8382anbi1d 630 . . . . . . . . . . . . . . 15 ((𝑧 = 0 ∧ 𝑥 = 0) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i))))
8483rexbidv 3177 . . . . . . . . . . . . . 14 ((𝑧 = 0 ∧ 𝑥 = 0) → (∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i))))
85 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 0 ∧ 𝑦 = 0) → 𝑦 = 0)
8685oveq1d 7408 . . . . . . . . . . . . . . . . 17 ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑦 · i) = (0 · i))
8786eqeq2d 2742 . . . . . . . . . . . . . . . 16 ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑧 = (𝑦 · i) ↔ 𝑧 = (0 · i)))
8887anbi2d 629 . . . . . . . . . . . . . . 15 ((𝑧 = 0 ∧ 𝑦 = 0) → ((𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i))))
8920mul02i 11385 . . . . . . . . . . . . . . . . . 18 (0 · 1) = 0
9089eqeq2i 2744 . . . . . . . . . . . . . . . . 17 (𝑧 = (0 · 1) ↔ 𝑧 = 0)
9190biimpri 227 . . . . . . . . . . . . . . . 16 (𝑧 = 0 → 𝑧 = (0 · 1))
9228mul02i 11385 . . . . . . . . . . . . . . . . . 18 (0 · i) = 0
9392eqeq2i 2744 . . . . . . . . . . . . . . . . 17 (𝑧 = (0 · i) ↔ 𝑧 = 0)
9493biimpri 227 . . . . . . . . . . . . . . . 16 (𝑧 = 0 → 𝑧 = (0 · i))
9591, 94jca 512 . . . . . . . . . . . . . . 15 (𝑧 = 0 → (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i)))
9679, 88, 95rspcedvd 3611 . . . . . . . . . . . . . 14 (𝑧 = 0 → ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)))
9779, 84, 96rspcedvd 3611 . . . . . . . . . . . . 13 (𝑧 = 0 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)))
9878, 97impbii 208 . . . . . . . . . . . 12 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ 𝑧 = 0)
9947, 48, 983bitr2i 298 . . . . . . . . . . 11 ((𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ 𝑧 = 0)
100 elin 3960 . . . . . . . . . . 11 (𝑧 ∈ (((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})))
101 velsn 4638 . . . . . . . . . . 11 (𝑧 ∈ {0} ↔ 𝑧 = 0)
10299, 100, 1013bitr4i 302 . . . . . . . . . 10 (𝑧 ∈ (((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ 𝑧 ∈ {0})
103102eqriv 2728 . . . . . . . . 9 (((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) = {0}
104103a1i 11 . . . . . . . 8 (⊤ → (((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) = {0})
1059, 18, 19, 27, 32, 104lindsun 32548 . . . . . . 7 (⊤ → ({1} ∪ {i}) ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
106105mptru 1548 . . . . . 6 ({1} ∪ {i}) ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
1078, 106eqeltri 2828 . . . . 5 {1, i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
108 cnfldadd 20883 . . . . . . . . . 10 + = (+g‘ℂfld)
10910, 16sraaddg 20743 . . . . . . . . . . 11 (⊤ → (+g‘ℂfld) = (+g‘((subringAlg ‘ℂfld)‘ℝ)))
110109mptru 1548 . . . . . . . . . 10 (+g‘ℂfld) = (+g‘((subringAlg ‘ℂfld)‘ℝ))
111108, 110eqtri 2759 . . . . . . . . 9 + = (+g‘((subringAlg ‘ℂfld)‘ℝ))
11234a1i 11 . . . . . . . . 9 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod)
113 1cnd 11191 . . . . . . . . 9 (⊤ → 1 ∈ ℂ)
11428a1i 11 . . . . . . . . 9 (⊤ → i ∈ ℂ)
11524, 111, 38, 4, 42, 9, 112, 113, 114lspprel 20654 . . . . . . . 8 (⊤ → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i))))
116115mptru 1548 . . . . . . 7 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)))
117 simpl 483 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ)
118117recnd 11224 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℂ)
119 1cnd 11191 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
120118, 119mulcld 11216 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 1) ∈ ℂ)
121 simpr 485 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
122121recnd 11224 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
12328a1i 11 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → i ∈ ℂ)
124122, 123mulcld 11216 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · i) ∈ ℂ)
125120, 124addcld 11215 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + (𝑦 · i)) ∈ ℂ)
126 eleq1 2820 . . . . . . . . . 10 (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → (𝑧 ∈ ℂ ↔ ((𝑥 · 1) + (𝑦 · i)) ∈ ℂ))
127125, 126syl5ibrcom 246 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈ ℂ))
128127rexlimivv 3198 . . . . . . . 8 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈ ℂ)
129 recl 15039 . . . . . . . . 9 (𝑧 ∈ ℂ → (ℜ‘𝑧) ∈ ℝ)
130 simpr 485 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → 𝑥 = (ℜ‘𝑧))
131130oveq1d 7408 . . . . . . . . . . . 12 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑥 · 1) = ((ℜ‘𝑧) · 1))
132131oveq1d 7408 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → ((𝑥 · 1) + (𝑦 · i)) = (((ℜ‘𝑧) · 1) + (𝑦 · i)))
133132eqeq2d 2742 . . . . . . . . . 10 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i))))
134133rexbidv 3177 . . . . . . . . 9 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i))))
135 imcl 15040 . . . . . . . . . 10 (𝑧 ∈ ℂ → (ℑ‘𝑧) ∈ ℝ)
136 simpr 485 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → 𝑦 = (ℑ‘𝑧))
137136oveq1d 7408 . . . . . . . . . . . 12 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑦 · i) = ((ℑ‘𝑧) · i))
138137oveq2d 7409 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (((ℜ‘𝑧) · 1) + (𝑦 · i)) = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)))
139138eqeq2d 2742 . . . . . . . . . 10 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i))))
140 replim 15045 . . . . . . . . . . 11 (𝑧 ∈ ℂ → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
141129recnd 11224 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → (ℜ‘𝑧) ∈ ℂ)
142141mulridd 11213 . . . . . . . . . . . 12 (𝑧 ∈ ℂ → ((ℜ‘𝑧) · 1) = (ℜ‘𝑧))
143135recnd 11224 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → (ℑ‘𝑧) ∈ ℂ)
14428a1i 11 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → i ∈ ℂ)
145143, 144mulcomd 11217 . . . . . . . . . . . 12 (𝑧 ∈ ℂ → ((ℑ‘𝑧) · i) = (i · (ℑ‘𝑧)))
146142, 145oveq12d 7411 . . . . . . . . . . 11 (𝑧 ∈ ℂ → (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)) = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
147140, 146eqtr4d 2774 . . . . . . . . . 10 (𝑧 ∈ ℂ → 𝑧 = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)))
148135, 139, 147rspcedvd 3611 . . . . . . . . 9 (𝑧 ∈ ℂ → ∃𝑦 ∈ ℝ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)))
149129, 134, 148rspcedvd 3611 . . . . . . . 8 (𝑧 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)))
150128, 149impbii 208 . . . . . . 7 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 ∈ ℂ)
151116, 150bitri 274 . . . . . 6 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ 𝑧 ∈ ℂ)
152151eqriv 2728 . . . . 5 ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) = ℂ
153 eqid 2731 . . . . . 6 (LBasis‘((subringAlg ‘ℂfld)‘ℝ)) = (LBasis‘((subringAlg ‘ℂfld)‘ℝ))
15424, 153, 9islbs4 21320 . . . . 5 ({1, i} ∈ (LBasis‘((subringAlg ‘ℂfld)‘ℝ)) ↔ ({1, i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)) ∧ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) = ℂ))
155107, 152, 154mpbir2an 709 . . . 4 {1, i} ∈ (LBasis‘((subringAlg ‘ℂfld)‘ℝ))
156153dimval 32525 . . . 4 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec ∧ {1, i} ∈ (LBasis‘((subringAlg ‘ℂfld)‘ℝ))) → (dim‘((subringAlg ‘ℂfld)‘ℝ)) = (♯‘{1, i}))
1577, 155, 156mp2an 690 . . 3 (dim‘((subringAlg ‘ℂfld)‘ℝ)) = (♯‘{1, i})
158 1nei 31832 . . . 4 1 ≠ i
159 hashprg 14337 . . . . 5 ((1 ∈ ℂ ∧ i ∈ ℂ) → (1 ≠ i ↔ (♯‘{1, i}) = 2))
16020, 28, 159mp2an 690 . . . 4 (1 ≠ i ↔ (♯‘{1, i}) = 2)
161158, 160mpbi 229 . . 3 (♯‘{1, i}) = 2
162157, 161eqtri 2759 . 2 (dim‘((subringAlg ‘ℂfld)‘ℝ)) = 2
1633, 6, 1623eqtr2i 2765 1 (ℂfld[:]ℝfld) = 2
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wtru 1542  wcel 2106  wne 2939  wrex 3069  cun 3942  cin 3943  wss 3944  {csn 4622  {cpr 4624   class class class wbr 5141  cfv 6532  (class class class)co 7393  cc 11090  cr 11091  0cc0 11092  1c1 11093  ici 11094   + caddc 11095   · cmul 11097  cmin 11426  -cneg 11427  2c2 12249  chash 14272  cre 15026  cim 15027  Basecbs 17126  s cress 17155  +gcplusg 17179  .rcmulr 17180  Scalarcsca 17182   ·𝑠 cvsca 17183  0gc0g 17367  LModclmod 20420  LSpanclspn 20531  LBasisclbs 20634  LVecclvec 20662  subringAlg csra 20730  fldccnfld 20878  fldcrefld 21090  LIndSclinds 21293  dimcldim 32523  /FldExtcfldext 32555  [:]cextdg 32558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-reg 9569  ax-inf2 9618  ax-ac2 10440  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169  ax-addf 11171  ax-mulf 11172
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-tp 4627  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-isom 6541  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-om 7839  df-1st 7957  df-2nd 7958  df-tpos 8193  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-oadd 8452  df-er 8686  df-map 8805  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-oi 9487  df-r1 9741  df-rank 9742  df-dju 9878  df-card 9916  df-acn 9919  df-ac 10093  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-div 11854  df-nn 12195  df-2 12257  df-3 12258  df-4 12259  df-5 12260  df-6 12261  df-7 12262  df-8 12263  df-9 12264  df-n0 12455  df-xnn0 12527  df-z 12541  df-dec 12660  df-uz 12805  df-fz 13467  df-hash 14273  df-cj 15028  df-re 15029  df-im 15030  df-struct 17062  df-sets 17079  df-slot 17097  df-ndx 17109  df-base 17127  df-ress 17156  df-plusg 17192  df-mulr 17193  df-starv 17194  df-sca 17195  df-vsca 17196  df-ip 17197  df-tset 17198  df-ple 17199  df-ocomp 17200  df-ds 17201  df-unif 17202  df-0g 17369  df-mre 17512  df-mrc 17513  df-mri 17514  df-acs 17515  df-proset 18230  df-drs 18231  df-poset 18248  df-ipo 18463  df-mgm 18543  df-sgrp 18592  df-mnd 18603  df-submnd 18648  df-grp 18797  df-minusg 18798  df-sbg 18799  df-subg 18975  df-cntz 19147  df-lsm 19468  df-cmn 19614  df-abl 19615  df-mgp 19947  df-ur 19964  df-ring 20016  df-cring 20017  df-oppr 20102  df-dvdsr 20123  df-unit 20124  df-invr 20154  df-dvr 20165  df-drng 20267  df-field 20268  df-subrg 20310  df-lmod 20422  df-lss 20492  df-lsp 20532  df-lbs 20635  df-lvec 20663  df-sra 20734  df-cnfld 20879  df-refld 21091  df-lindf 21294  df-linds 21295  df-dim 32524  df-fldext 32559  df-extdg 32560
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator