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 32356
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 32337 . . 3 fld/FldExtfld
2 extdgval 32343 . . 3 (ℂfld/FldExtfld → (ℂfld[:]ℝfld) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld))))
31, 2ax-mp 5 . 2 (ℂfld[:]ℝfld) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld)))
4 rebase 21010 . . . 4 ℝ = (Base‘ℝfld)
54fveq2i 6845 . . 3 ((subringAlg ‘ℂfld)‘ℝ) = ((subringAlg ‘ℂfld)‘(Base‘ℝfld))
65fveq2i 6845 . 2 (dim‘((subringAlg ‘ℂfld)‘ℝ)) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld)))
7 ccfldsrarelvec 32355 . . . 4 ((subringAlg ‘ℂfld)‘ℝ) ∈ LVec
8 df-pr 4589 . . . . . 6 {1, i} = ({1} ∪ {i})
9 eqid 2736 . . . . . . . 8 (LSpan‘((subringAlg ‘ℂfld)‘ℝ)) = (LSpan‘((subringAlg ‘ℂfld)‘ℝ))
10 eqidd 2737 . . . . . . . . . 10 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) = ((subringAlg ‘ℂfld)‘ℝ))
11 cnfld0 20821 . . . . . . . . . . 11 0 = (0g‘ℂfld)
1211a1i 11 . . . . . . . . . 10 (⊤ → 0 = (0g‘ℂfld))
13 ax-resscn 11108 . . . . . . . . . . . 12 ℝ ⊆ ℂ
14 cnfldbas 20800 . . . . . . . . . . . 12 ℂ = (Base‘ℂfld)
1513, 14sseqtri 3980 . . . . . . . . . . 11 ℝ ⊆ (Base‘ℂfld)
1615a1i 11 . . . . . . . . . 10 (⊤ → ℝ ⊆ (Base‘ℂfld))
1710, 12, 16sralmod0 20657 . . . . . . . . 9 (⊤ → 0 = (0g‘((subringAlg ‘ℂfld)‘ℝ)))
1817mptru 1548 . . . . . . . 8 0 = (0g‘((subringAlg ‘ℂfld)‘ℝ))
197a1i 11 . . . . . . . 8 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) ∈ LVec)
20 ax-1cn 11109 . . . . . . . . . 10 1 ∈ ℂ
21 ax-1ne0 11120 . . . . . . . . . 10 1 ≠ 0
2210, 16srabase 20640 . . . . . . . . . . . . 13 (⊤ → (Base‘ℂfld) = (Base‘((subringAlg ‘ℂfld)‘ℝ)))
2322mptru 1548 . . . . . . . . . . . 12 (Base‘ℂfld) = (Base‘((subringAlg ‘ℂfld)‘ℝ))
2414, 23eqtri 2764 . . . . . . . . . . 11 ℂ = (Base‘((subringAlg ‘ℂfld)‘ℝ))
2524, 18lindssn 32166 . . . . . . . . . 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 11110 . . . . . . . . . 10 i ∈ ℂ
29 ine0 11590 . . . . . . . . . 10 i ≠ 0
3024, 18lindssn 32166 . . . . . . . . . 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 20567 . . . . . . . . . . . . . . 15 (((subringAlg ‘ℂfld)‘ℝ) ∈ LVec → ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod)
347, 33ax-mp 5 . . . . . . . . . . . . . 14 ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod
35 df-refld 21009 . . . . . . . . . . . . . . . 16 fld = (ℂflds ℝ)
3610, 16srasca 20646 . . . . . . . . . . . . . . . . 17 (⊤ → (ℂflds ℝ) = (Scalar‘((subringAlg ‘ℂfld)‘ℝ)))
3736mptru 1548 . . . . . . . . . . . . . . . 16 (ℂflds ℝ) = (Scalar‘((subringAlg ‘ℂfld)‘ℝ))
3835, 37eqtri 2764 . . . . . . . . . . . . . . 15 fld = (Scalar‘((subringAlg ‘ℂfld)‘ℝ))
39 cnfldmul 20802 . . . . . . . . . . . . . . . 16 · = (.r‘ℂfld)
4010, 16sravsca 20648 . . . . . . . . . . . . . . . . 17 (⊤ → (.r‘ℂfld) = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ)))
4140mptru 1548 . . . . . . . . . . . . . . . 16 (.r‘ℂfld) = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ))
4239, 41eqtri 2764 . . . . . . . . . . . . . . 15 · = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ))
4338, 4, 24, 42, 9lspsnel 20464 . . . . . . . . . . . . . 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 20464 . . . . . . . . . . . . . 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 3217 . . . . . . . . . . . 12 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1) ∧ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
49 simprl 769 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑥 · 1))
50 simpll 765 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℝ)
5150recnd 11183 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℂ)
5251mulid1d 11172 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑥 · 1) = 𝑥)
5349, 52eqtrd 2776 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 𝑥)
5453negeqd 11395 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑧 = -𝑥)
55 simprr 771 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑦 · i))
56 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℝ)
5756recnd 11183 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℂ)
5828a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → i ∈ ℂ)
5957, 58mulcomd 11176 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑦 · i) = (i · 𝑦))
6055, 59eqtrd 2776 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (i · 𝑦))
6154, 60oveq12d 7375 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = (-𝑥 + (i · 𝑦)))
6253, 51eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 ∈ ℂ)
6362subidd 11500 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑧𝑧) = 0)
6463negeqd 11395 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧𝑧) = -0)
6562, 62negsubdid 11527 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧𝑧) = (-𝑧 + 𝑧))
66 neg0 11447 . . . . . . . . . . . . . . . . . . . . . 22 -0 = 0
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 = 0)
6864, 65, 673eqtr3d 2784 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = 0)
6961, 68eqtr3d 2778 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑥 + (i · 𝑦)) = 0)
7050renegcld 11582 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑥 ∈ ℝ)
71 creq0 31652 . . . . . . . . . . . . . . . . . . . 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 11507 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 = 𝑥)
7653, 75, 673eqtr2d 2782 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 0)
7776ex 413 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0))
7877rexlimivv 3196 . . . . . . . . . . . . 13 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0)
79 0red 11158 . . . . . . . . . . . . . 14 (𝑧 = 0 → 0 ∈ ℝ)
80 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 0 ∧ 𝑥 = 0) → 𝑥 = 0)
8180oveq1d 7372 . . . . . . . . . . . . . . . . 17 ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑥 · 1) = (0 · 1))
8281eqeq2d 2747 . . . . . . . . . . . . . . . 16 ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑧 = (𝑥 · 1) ↔ 𝑧 = (0 · 1)))
8382anbi1d 630 . . . . . . . . . . . . . . 15 ((𝑧 = 0 ∧ 𝑥 = 0) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i))))
8483rexbidv 3175 . . . . . . . . . . . . . 14 ((𝑧 = 0 ∧ 𝑥 = 0) → (∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i))))
85 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 0 ∧ 𝑦 = 0) → 𝑦 = 0)
8685oveq1d 7372 . . . . . . . . . . . . . . . . 17 ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑦 · i) = (0 · i))
8786eqeq2d 2747 . . . . . . . . . . . . . . . 16 ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑧 = (𝑦 · i) ↔ 𝑧 = (0 · i)))
8887anbi2d 629 . . . . . . . . . . . . . . 15 ((𝑧 = 0 ∧ 𝑦 = 0) → ((𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i))))
8920mul02i 11344 . . . . . . . . . . . . . . . . . 18 (0 · 1) = 0
9089eqeq2i 2749 . . . . . . . . . . . . . . . . 17 (𝑧 = (0 · 1) ↔ 𝑧 = 0)
9190biimpri 227 . . . . . . . . . . . . . . . 16 (𝑧 = 0 → 𝑧 = (0 · 1))
9228mul02i 11344 . . . . . . . . . . . . . . . . . 18 (0 · i) = 0
9392eqeq2i 2749 . . . . . . . . . . . . . . . . 17 (𝑧 = (0 · i) ↔ 𝑧 = 0)
9493biimpri 227 . . . . . . . . . . . . . . . 16 (𝑧 = 0 → 𝑧 = (0 · i))
9591, 94jca 512 . . . . . . . . . . . . . . 15 (𝑧 = 0 → (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i)))
9679, 88, 95rspcedvd 3583 . . . . . . . . . . . . . 14 (𝑧 = 0 → ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)))
9779, 84, 96rspcedvd 3583 . . . . . . . . . . . . 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 3926 . . . . . . . . . . 11 (𝑧 ∈ (((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})))
101 velsn 4602 . . . . . . . . . . 11 (𝑧 ∈ {0} ↔ 𝑧 = 0)
10299, 100, 1013bitr4i 302 . . . . . . . . . 10 (𝑧 ∈ (((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ 𝑧 ∈ {0})
103102eqriv 2733 . . . . . . . . 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 32320 . . . . . . 7 (⊤ → ({1} ∪ {i}) ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
106105mptru 1548 . . . . . 6 ({1} ∪ {i}) ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
1078, 106eqeltri 2834 . . . . 5 {1, i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
108 cnfldadd 20801 . . . . . . . . . 10 + = (+g‘ℂfld)
10910, 16sraaddg 20642 . . . . . . . . . . 11 (⊤ → (+g‘ℂfld) = (+g‘((subringAlg ‘ℂfld)‘ℝ)))
110109mptru 1548 . . . . . . . . . 10 (+g‘ℂfld) = (+g‘((subringAlg ‘ℂfld)‘ℝ))
111108, 110eqtri 2764 . . . . . . . . 9 + = (+g‘((subringAlg ‘ℂfld)‘ℝ))
11234a1i 11 . . . . . . . . 9 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod)
113 1cnd 11150 . . . . . . . . 9 (⊤ → 1 ∈ ℂ)
11428a1i 11 . . . . . . . . 9 (⊤ → i ∈ ℂ)
11524, 111, 38, 4, 42, 9, 112, 113, 114lspprel 20555 . . . . . . . 8 (⊤ → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i))))
116115mptru 1548 . . . . . . 7 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)))
117 simpl 483 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ)
118117recnd 11183 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℂ)
119 1cnd 11150 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
120118, 119mulcld 11175 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 1) ∈ ℂ)
121 simpr 485 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
122121recnd 11183 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
12328a1i 11 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → i ∈ ℂ)
124122, 123mulcld 11175 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · i) ∈ ℂ)
125120, 124addcld 11174 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + (𝑦 · i)) ∈ ℂ)
126 eleq1 2825 . . . . . . . . . 10 (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → (𝑧 ∈ ℂ ↔ ((𝑥 · 1) + (𝑦 · i)) ∈ ℂ))
127125, 126syl5ibrcom 246 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈ ℂ))
128127rexlimivv 3196 . . . . . . . 8 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈ ℂ)
129 recl 14995 . . . . . . . . 9 (𝑧 ∈ ℂ → (ℜ‘𝑧) ∈ ℝ)
130 simpr 485 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → 𝑥 = (ℜ‘𝑧))
131130oveq1d 7372 . . . . . . . . . . . 12 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑥 · 1) = ((ℜ‘𝑧) · 1))
132131oveq1d 7372 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → ((𝑥 · 1) + (𝑦 · i)) = (((ℜ‘𝑧) · 1) + (𝑦 · i)))
133132eqeq2d 2747 . . . . . . . . . 10 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i))))
134133rexbidv 3175 . . . . . . . . 9 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i))))
135 imcl 14996 . . . . . . . . . 10 (𝑧 ∈ ℂ → (ℑ‘𝑧) ∈ ℝ)
136 simpr 485 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → 𝑦 = (ℑ‘𝑧))
137136oveq1d 7372 . . . . . . . . . . . 12 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑦 · i) = ((ℑ‘𝑧) · i))
138137oveq2d 7373 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (((ℜ‘𝑧) · 1) + (𝑦 · i)) = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)))
139138eqeq2d 2747 . . . . . . . . . 10 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i))))
140 replim 15001 . . . . . . . . . . 11 (𝑧 ∈ ℂ → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
141129recnd 11183 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → (ℜ‘𝑧) ∈ ℂ)
142141mulid1d 11172 . . . . . . . . . . . 12 (𝑧 ∈ ℂ → ((ℜ‘𝑧) · 1) = (ℜ‘𝑧))
143135recnd 11183 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → (ℑ‘𝑧) ∈ ℂ)
14428a1i 11 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → i ∈ ℂ)
145143, 144mulcomd 11176 . . . . . . . . . . . 12 (𝑧 ∈ ℂ → ((ℑ‘𝑧) · i) = (i · (ℑ‘𝑧)))
146142, 145oveq12d 7375 . . . . . . . . . . 11 (𝑧 ∈ ℂ → (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)) = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
147140, 146eqtr4d 2779 . . . . . . . . . 10 (𝑧 ∈ ℂ → 𝑧 = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)))
148135, 139, 147rspcedvd 3583 . . . . . . . . 9 (𝑧 ∈ ℂ → ∃𝑦 ∈ ℝ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)))
149129, 134, 148rspcedvd 3583 . . . . . . . 8 (𝑧 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)))
150128, 149impbii 208 . . . . . . 7 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 ∈ ℂ)
151116, 150bitri 274 . . . . . 6 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ 𝑧 ∈ ℂ)
152151eqriv 2733 . . . . 5 ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) = ℂ
153 eqid 2736 . . . . . 6 (LBasis‘((subringAlg ‘ℂfld)‘ℝ)) = (LBasis‘((subringAlg ‘ℂfld)‘ℝ))
15424, 153, 9islbs4 21238 . . . . 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 32300 . . . 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 31653 . . . 4 1 ≠ i
159 hashprg 14295 . . . . 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 2764 . 2 (dim‘((subringAlg ‘ℂfld)‘ℝ)) = 2
1633, 6, 1623eqtr2i 2770 1 (ℂfld[:]ℝfld) = 2
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wtru 1542  wcel 2106  wne 2943  wrex 3073  cun 3908  cin 3909  wss 3910  {csn 4586  {cpr 4588   class class class wbr 5105  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052  ici 11053   + caddc 11054   · cmul 11056  cmin 11385  -cneg 11386  2c2 12208  chash 14230  cre 14982  cim 14983  Basecbs 17083  s cress 17112  +gcplusg 17133  .rcmulr 17134  Scalarcsca 17136   ·𝑠 cvsca 17137  0gc0g 17321  LModclmod 20322  LSpanclspn 20432  LBasisclbs 20535  LVecclvec 20563  subringAlg csra 20629  fldccnfld 20796  fldcrefld 21008  LIndSclinds 21211  dimcldim 32298  /FldExtcfldext 32327  [:]cextdg 32330
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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-reg 9528  ax-inf2 9577  ax-ac2 10399  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-addf 11130  ax-mulf 11131
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-tpos 8157  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-oi 9446  df-r1 9700  df-rank 9701  df-dju 9837  df-card 9875  df-acn 9878  df-ac 10052  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-xnn0 12486  df-z 12500  df-dec 12619  df-uz 12764  df-fz 13425  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ocomp 17154  df-ds 17155  df-unif 17156  df-0g 17323  df-mre 17466  df-mrc 17467  df-mri 17468  df-acs 17469  df-proset 18184  df-drs 18185  df-poset 18202  df-ipo 18417  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-grp 18751  df-minusg 18752  df-sbg 18753  df-subg 18925  df-cntz 19097  df-lsm 19418  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-ring 19966  df-cring 19967  df-oppr 20049  df-dvdsr 20070  df-unit 20071  df-invr 20101  df-dvr 20112  df-drng 20187  df-field 20188  df-subrg 20220  df-lmod 20324  df-lss 20393  df-lsp 20433  df-lbs 20536  df-lvec 20564  df-sra 20633  df-cnfld 20797  df-refld 21009  df-lindf 21212  df-linds 21213  df-dim 32299  df-fldext 32331  df-extdg 32332
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator