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 33697
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 33676 . . 3 fld/FldExtfld
2 extdgval 33682 . . 3 (ℂfld/FldExtfld → (ℂfld[:]ℝfld) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld))))
31, 2ax-mp 5 . 2 (ℂfld[:]ℝfld) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld)))
4 rebase 21642 . . . 4 ℝ = (Base‘ℝfld)
54fveq2i 6910 . . 3 ((subringAlg ‘ℂfld)‘ℝ) = ((subringAlg ‘ℂfld)‘(Base‘ℝfld))
65fveq2i 6910 . 2 (dim‘((subringAlg ‘ℂfld)‘ℝ)) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld)))
7 ccfldsrarelvec 33696 . . . 4 ((subringAlg ‘ℂfld)‘ℝ) ∈ LVec
8 df-pr 4634 . . . . . 6 {1, i} = ({1} ∪ {i})
9 eqid 2735 . . . . . . . 8 (LSpan‘((subringAlg ‘ℂfld)‘ℝ)) = (LSpan‘((subringAlg ‘ℂfld)‘ℝ))
10 eqidd 2736 . . . . . . . . . 10 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) = ((subringAlg ‘ℂfld)‘ℝ))
11 cnfld0 21423 . . . . . . . . . . 11 0 = (0g‘ℂfld)
1211a1i 11 . . . . . . . . . 10 (⊤ → 0 = (0g‘ℂfld))
13 ax-resscn 11210 . . . . . . . . . . . 12 ℝ ⊆ ℂ
14 cnfldbas 21386 . . . . . . . . . . . 12 ℂ = (Base‘ℂfld)
1513, 14sseqtri 4032 . . . . . . . . . . 11 ℝ ⊆ (Base‘ℂfld)
1615a1i 11 . . . . . . . . . 10 (⊤ → ℝ ⊆ (Base‘ℂfld))
1710, 12, 16sralmod0 21213 . . . . . . . . 9 (⊤ → 0 = (0g‘((subringAlg ‘ℂfld)‘ℝ)))
1817mptru 1544 . . . . . . . 8 0 = (0g‘((subringAlg ‘ℂfld)‘ℝ))
197a1i 11 . . . . . . . 8 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) ∈ LVec)
20 ax-1cn 11211 . . . . . . . . . 10 1 ∈ ℂ
21 ax-1ne0 11222 . . . . . . . . . 10 1 ≠ 0
2210, 16srabase 21195 . . . . . . . . . . . . 13 (⊤ → (Base‘ℂfld) = (Base‘((subringAlg ‘ℂfld)‘ℝ)))
2322mptru 1544 . . . . . . . . . . . 12 (Base‘ℂfld) = (Base‘((subringAlg ‘ℂfld)‘ℝ))
2414, 23eqtri 2763 . . . . . . . . . . 11 ℂ = (Base‘((subringAlg ‘ℂfld)‘ℝ))
2524, 18lindssn 33386 . . . . . . . . . 10 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → {1} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
267, 20, 21, 25mp3an 1460 . . . . . . . . 9 {1} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
2726a1i 11 . . . . . . . 8 (⊤ → {1} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
28 ax-icn 11212 . . . . . . . . . 10 i ∈ ℂ
29 ine0 11696 . . . . . . . . . 10 i ≠ 0
3024, 18lindssn 33386 . . . . . . . . . 10 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec ∧ i ∈ ℂ ∧ i ≠ 0) → {i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
317, 28, 29, 30mp3an 1460 . . . . . . . . 9 {i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
3231a1i 11 . . . . . . . 8 (⊤ → {i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
33 lveclmod 21123 . . . . . . . . . . . . . . 15 (((subringAlg ‘ℂfld)‘ℝ) ∈ LVec → ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod)
347, 33ax-mp 5 . . . . . . . . . . . . . 14 ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod
35 df-refld 21641 . . . . . . . . . . . . . . . 16 fld = (ℂflds ℝ)
3610, 16srasca 21201 . . . . . . . . . . . . . . . . 17 (⊤ → (ℂflds ℝ) = (Scalar‘((subringAlg ‘ℂfld)‘ℝ)))
3736mptru 1544 . . . . . . . . . . . . . . . 16 (ℂflds ℝ) = (Scalar‘((subringAlg ‘ℂfld)‘ℝ))
3835, 37eqtri 2763 . . . . . . . . . . . . . . 15 fld = (Scalar‘((subringAlg ‘ℂfld)‘ℝ))
39 cnfldmul 21390 . . . . . . . . . . . . . . . 16 · = (.r‘ℂfld)
4010, 16sravsca 21203 . . . . . . . . . . . . . . . . 17 (⊤ → (.r‘ℂfld) = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ)))
4140mptru 1544 . . . . . . . . . . . . . . . 16 (.r‘ℂfld) = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ))
4239, 41eqtri 2763 . . . . . . . . . . . . . . 15 · = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ))
4338, 4, 24, 42, 9ellspsn 21019 . . . . . . . . . . . . . 14 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LMod ∧ 1 ∈ ℂ) → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ↔ ∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1)))
4434, 20, 43mp2an 692 . . . . . . . . . . . . 13 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ↔ ∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1))
4538, 4, 24, 42, 9ellspsn 21019 . . . . . . . . . . . . . 14 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LMod ∧ i ∈ ℂ) → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i}) ↔ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
4634, 28, 45mp2an 692 . . . . . . . . . . . . 13 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i}) ↔ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i))
4744, 46anbi12i 628 . . . . . . . . . . . 12 ((𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ (∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1) ∧ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
48 reeanv 3227 . . . . . . . . . . . 12 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1) ∧ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
49 simprl 771 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑥 · 1))
50 simpll 767 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℝ)
5150recnd 11287 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℂ)
5251mulridd 11276 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑥 · 1) = 𝑥)
5349, 52eqtrd 2775 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 𝑥)
5453negeqd 11500 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑧 = -𝑥)
55 simprr 773 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑦 · i))
56 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℝ)
5756recnd 11287 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℂ)
5828a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → i ∈ ℂ)
5957, 58mulcomd 11280 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑦 · i) = (i · 𝑦))
6055, 59eqtrd 2775 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (i · 𝑦))
6154, 60oveq12d 7449 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = (-𝑥 + (i · 𝑦)))
6253, 51eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 ∈ ℂ)
6362subidd 11606 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑧𝑧) = 0)
6463negeqd 11500 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧𝑧) = -0)
6562, 62negsubdid 11633 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧𝑧) = (-𝑧 + 𝑧))
66 neg0 11553 . . . . . . . . . . . . . . . . . . . . . 22 -0 = 0
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 = 0)
6864, 65, 673eqtr3d 2783 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = 0)
6961, 68eqtr3d 2777 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑥 + (i · 𝑦)) = 0)
7050renegcld 11688 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑥 ∈ ℝ)
71 creq0 32753 . . . . . . . . . . . . . . . . . . . 20 ((-𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((-𝑥 = 0 ∧ 𝑦 = 0) ↔ (-𝑥 + (i · 𝑦)) = 0))
7270, 56, 71syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → ((-𝑥 = 0 ∧ 𝑦 = 0) ↔ (-𝑥 + (i · 𝑦)) = 0))
7369, 72mpbird 257 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑥 = 0 ∧ 𝑦 = 0))
7473simpld 494 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑥 = 0)
7551, 74negcon1ad 11613 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 = 𝑥)
7653, 75, 673eqtr2d 2781 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 0)
7776ex 412 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0))
7877rexlimivv 3199 . . . . . . . . . . . . 13 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0)
79 0red 11262 . . . . . . . . . . . . . 14 (𝑧 = 0 → 0 ∈ ℝ)
80 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 0 ∧ 𝑥 = 0) → 𝑥 = 0)
8180oveq1d 7446 . . . . . . . . . . . . . . . . 17 ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑥 · 1) = (0 · 1))
8281eqeq2d 2746 . . . . . . . . . . . . . . . 16 ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑧 = (𝑥 · 1) ↔ 𝑧 = (0 · 1)))
8382anbi1d 631 . . . . . . . . . . . . . . 15 ((𝑧 = 0 ∧ 𝑥 = 0) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i))))
8483rexbidv 3177 . . . . . . . . . . . . . 14 ((𝑧 = 0 ∧ 𝑥 = 0) → (∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i))))
85 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 0 ∧ 𝑦 = 0) → 𝑦 = 0)
8685oveq1d 7446 . . . . . . . . . . . . . . . . 17 ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑦 · i) = (0 · i))
8786eqeq2d 2746 . . . . . . . . . . . . . . . 16 ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑧 = (𝑦 · i) ↔ 𝑧 = (0 · i)))
8887anbi2d 630 . . . . . . . . . . . . . . 15 ((𝑧 = 0 ∧ 𝑦 = 0) → ((𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i))))
8920mul02i 11448 . . . . . . . . . . . . . . . . . 18 (0 · 1) = 0
9089eqeq2i 2748 . . . . . . . . . . . . . . . . 17 (𝑧 = (0 · 1) ↔ 𝑧 = 0)
9190biimpri 228 . . . . . . . . . . . . . . . 16 (𝑧 = 0 → 𝑧 = (0 · 1))
9228mul02i 11448 . . . . . . . . . . . . . . . . . 18 (0 · i) = 0
9392eqeq2i 2748 . . . . . . . . . . . . . . . . 17 (𝑧 = (0 · i) ↔ 𝑧 = 0)
9493biimpri 228 . . . . . . . . . . . . . . . 16 (𝑧 = 0 → 𝑧 = (0 · i))
9591, 94jca 511 . . . . . . . . . . . . . . 15 (𝑧 = 0 → (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i)))
9679, 88, 95rspcedvd 3624 . . . . . . . . . . . . . 14 (𝑧 = 0 → ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)))
9779, 84, 96rspcedvd 3624 . . . . . . . . . . . . 13 (𝑧 = 0 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)))
9878, 97impbii 209 . . . . . . . . . . . 12 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ 𝑧 = 0)
9947, 48, 983bitr2i 299 . . . . . . . . . . 11 ((𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ 𝑧 = 0)
100 elin 3979 . . . . . . . . . . 11 (𝑧 ∈ (((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})))
101 velsn 4647 . . . . . . . . . . 11 (𝑧 ∈ {0} ↔ 𝑧 = 0)
10299, 100, 1013bitr4i 303 . . . . . . . . . 10 (𝑧 ∈ (((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ 𝑧 ∈ {0})
103102eqriv 2732 . . . . . . . . 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 33653 . . . . . . 7 (⊤ → ({1} ∪ {i}) ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
106105mptru 1544 . . . . . 6 ({1} ∪ {i}) ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
1078, 106eqeltri 2835 . . . . 5 {1, i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
108 cnfldadd 21388 . . . . . . . . . 10 + = (+g‘ℂfld)
10910, 16sraaddg 21197 . . . . . . . . . . 11 (⊤ → (+g‘ℂfld) = (+g‘((subringAlg ‘ℂfld)‘ℝ)))
110109mptru 1544 . . . . . . . . . 10 (+g‘ℂfld) = (+g‘((subringAlg ‘ℂfld)‘ℝ))
111108, 110eqtri 2763 . . . . . . . . 9 + = (+g‘((subringAlg ‘ℂfld)‘ℝ))
11234a1i 11 . . . . . . . . 9 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod)
113 1cnd 11254 . . . . . . . . 9 (⊤ → 1 ∈ ℂ)
11428a1i 11 . . . . . . . . 9 (⊤ → i ∈ ℂ)
11524, 111, 38, 4, 42, 9, 112, 113, 114lspprel 21111 . . . . . . . 8 (⊤ → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i))))
116115mptru 1544 . . . . . . 7 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)))
117 simpl 482 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ)
118117recnd 11287 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℂ)
119 1cnd 11254 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
120118, 119mulcld 11279 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 1) ∈ ℂ)
121 simpr 484 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
122121recnd 11287 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
12328a1i 11 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → i ∈ ℂ)
124122, 123mulcld 11279 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · i) ∈ ℂ)
125120, 124addcld 11278 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + (𝑦 · i)) ∈ ℂ)
126 eleq1 2827 . . . . . . . . . 10 (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → (𝑧 ∈ ℂ ↔ ((𝑥 · 1) + (𝑦 · i)) ∈ ℂ))
127125, 126syl5ibrcom 247 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈ ℂ))
128127rexlimivv 3199 . . . . . . . 8 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈ ℂ)
129 recl 15146 . . . . . . . . 9 (𝑧 ∈ ℂ → (ℜ‘𝑧) ∈ ℝ)
130 simpr 484 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → 𝑥 = (ℜ‘𝑧))
131130oveq1d 7446 . . . . . . . . . . . 12 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑥 · 1) = ((ℜ‘𝑧) · 1))
132131oveq1d 7446 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → ((𝑥 · 1) + (𝑦 · i)) = (((ℜ‘𝑧) · 1) + (𝑦 · i)))
133132eqeq2d 2746 . . . . . . . . . 10 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i))))
134133rexbidv 3177 . . . . . . . . 9 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i))))
135 imcl 15147 . . . . . . . . . 10 (𝑧 ∈ ℂ → (ℑ‘𝑧) ∈ ℝ)
136 simpr 484 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → 𝑦 = (ℑ‘𝑧))
137136oveq1d 7446 . . . . . . . . . . . 12 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑦 · i) = ((ℑ‘𝑧) · i))
138137oveq2d 7447 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (((ℜ‘𝑧) · 1) + (𝑦 · i)) = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)))
139138eqeq2d 2746 . . . . . . . . . 10 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i))))
140 replim 15152 . . . . . . . . . . 11 (𝑧 ∈ ℂ → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
141129recnd 11287 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → (ℜ‘𝑧) ∈ ℂ)
142141mulridd 11276 . . . . . . . . . . . 12 (𝑧 ∈ ℂ → ((ℜ‘𝑧) · 1) = (ℜ‘𝑧))
143135recnd 11287 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → (ℑ‘𝑧) ∈ ℂ)
14428a1i 11 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → i ∈ ℂ)
145143, 144mulcomd 11280 . . . . . . . . . . . 12 (𝑧 ∈ ℂ → ((ℑ‘𝑧) · i) = (i · (ℑ‘𝑧)))
146142, 145oveq12d 7449 . . . . . . . . . . 11 (𝑧 ∈ ℂ → (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)) = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
147140, 146eqtr4d 2778 . . . . . . . . . 10 (𝑧 ∈ ℂ → 𝑧 = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)))
148135, 139, 147rspcedvd 3624 . . . . . . . . 9 (𝑧 ∈ ℂ → ∃𝑦 ∈ ℝ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)))
149129, 134, 148rspcedvd 3624 . . . . . . . 8 (𝑧 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)))
150128, 149impbii 209 . . . . . . 7 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 ∈ ℂ)
151116, 150bitri 275 . . . . . 6 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ 𝑧 ∈ ℂ)
152151eqriv 2732 . . . . 5 ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) = ℂ
153 eqid 2735 . . . . . 6 (LBasis‘((subringAlg ‘ℂfld)‘ℝ)) = (LBasis‘((subringAlg ‘ℂfld)‘ℝ))
15424, 153, 9islbs4 21870 . . . . 5 ({1, i} ∈ (LBasis‘((subringAlg ‘ℂfld)‘ℝ)) ↔ ({1, i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)) ∧ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) = ℂ))
155107, 152, 154mpbir2an 711 . . . 4 {1, i} ∈ (LBasis‘((subringAlg ‘ℂfld)‘ℝ))
156153dimval 33628 . . . 4 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec ∧ {1, i} ∈ (LBasis‘((subringAlg ‘ℂfld)‘ℝ))) → (dim‘((subringAlg ‘ℂfld)‘ℝ)) = (♯‘{1, i}))
1577, 155, 156mp2an 692 . . 3 (dim‘((subringAlg ‘ℂfld)‘ℝ)) = (♯‘{1, i})
158 1nei 32754 . . . 4 1 ≠ i
159 hashprg 14431 . . . . 5 ((1 ∈ ℂ ∧ i ∈ ℂ) → (1 ≠ i ↔ (♯‘{1, i}) = 2))
16020, 28, 159mp2an 692 . . . 4 (1 ≠ i ↔ (♯‘{1, i}) = 2)
161158, 160mpbi 230 . . 3 (♯‘{1, i}) = 2
162157, 161eqtri 2763 . 2 (dim‘((subringAlg ‘ℂfld)‘ℝ)) = 2
1633, 6, 1623eqtr2i 2769 1 (ℂfld[:]ℝfld) = 2
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1537  wtru 1538  wcel 2106  wne 2938  wrex 3068  cun 3961  cin 3962  wss 3963  {csn 4631  {cpr 4633   class class class wbr 5148  cfv 6563  (class class class)co 7431  cc 11151  cr 11152  0cc0 11153  1c1 11154  ici 11155   + caddc 11156   · cmul 11158  cmin 11490  -cneg 11491  2c2 12319  chash 14366  cre 15133  cim 15134  Basecbs 17245  s cress 17274  +gcplusg 17298  .rcmulr 17299  Scalarcsca 17301   ·𝑠 cvsca 17302  0gc0g 17486  LModclmod 20875  LSpanclspn 20987  LBasisclbs 21091  LVecclvec 21119  subringAlg csra 21188  fldccnfld 21382  fldcrefld 21640  LIndSclinds 21843  dimcldim 33626  /FldExtcfldext 33666  [:]cextdg 33669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-reg 9630  ax-inf2 9679  ax-ac2 10501  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-addf 11232  ax-mulf 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-tpos 8250  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-oadd 8509  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-oi 9548  df-r1 9802  df-rank 9803  df-dju 9939  df-card 9977  df-acn 9980  df-ac 10154  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-xnn0 12598  df-z 12612  df-dec 12732  df-uz 12877  df-fz 13545  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ocomp 17319  df-ds 17320  df-unif 17321  df-0g 17488  df-mre 17631  df-mrc 17632  df-mri 17633  df-acs 17634  df-proset 18352  df-drs 18353  df-poset 18371  df-ipo 18586  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-submnd 18810  df-grp 18967  df-minusg 18968  df-sbg 18969  df-subg 19154  df-cntz 19348  df-lsm 19669  df-cmn 19815  df-abl 19816  df-mgp 20153  df-rng 20171  df-ur 20200  df-ring 20253  df-cring 20254  df-oppr 20351  df-dvdsr 20374  df-unit 20375  df-invr 20405  df-dvr 20418  df-subrng 20563  df-subrg 20587  df-drng 20748  df-field 20749  df-lmod 20877  df-lss 20948  df-lsp 20988  df-lbs 21092  df-lvec 21120  df-sra 21190  df-cnfld 21383  df-refld 21641  df-lindf 21844  df-linds 21845  df-dim 33627  df-fldext 33670  df-extdg 33671
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator