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 30657
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 30638 . . 3 fld/FldExtfld
2 extdgval 30644 . . 3 (ℂfld/FldExtfld → (ℂfld[:]ℝfld) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld))))
31, 2ax-mp 5 . 2 (ℂfld[:]ℝfld) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld)))
4 rebase 20436 . . . 4 ℝ = (Base‘ℝfld)
54fveq2i 6548 . . 3 ((subringAlg ‘ℂfld)‘ℝ) = ((subringAlg ‘ℂfld)‘(Base‘ℝfld))
65fveq2i 6548 . 2 (dim‘((subringAlg ‘ℂfld)‘ℝ)) = (dim‘((subringAlg ‘ℂfld)‘(Base‘ℝfld)))
7 ccfldsrarelvec 30656 . . . 4 ((subringAlg ‘ℂfld)‘ℝ) ∈ LVec
8 df-pr 4481 . . . . . 6 {1, i} = ({1} ∪ {i})
9 eqid 2797 . . . . . . . 8 (LSpan‘((subringAlg ‘ℂfld)‘ℝ)) = (LSpan‘((subringAlg ‘ℂfld)‘ℝ))
10 eqidd 2798 . . . . . . . . . 10 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) = ((subringAlg ‘ℂfld)‘ℝ))
11 cnfld0 20255 . . . . . . . . . . 11 0 = (0g‘ℂfld)
1211a1i 11 . . . . . . . . . 10 (⊤ → 0 = (0g‘ℂfld))
13 ax-resscn 10447 . . . . . . . . . . . 12 ℝ ⊆ ℂ
14 cnfldbas 20235 . . . . . . . . . . . 12 ℂ = (Base‘ℂfld)
1513, 14sseqtri 3930 . . . . . . . . . . 11 ℝ ⊆ (Base‘ℂfld)
1615a1i 11 . . . . . . . . . 10 (⊤ → ℝ ⊆ (Base‘ℂfld))
1710, 12, 16sralmod0 19654 . . . . . . . . 9 (⊤ → 0 = (0g‘((subringAlg ‘ℂfld)‘ℝ)))
1817mptru 1532 . . . . . . . 8 0 = (0g‘((subringAlg ‘ℂfld)‘ℝ))
197a1i 11 . . . . . . . 8 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) ∈ LVec)
20 ax-1cn 10448 . . . . . . . . . 10 1 ∈ ℂ
21 ax-1ne0 10459 . . . . . . . . . 10 1 ≠ 0
2210, 16srabase 19644 . . . . . . . . . . . . 13 (⊤ → (Base‘ℂfld) = (Base‘((subringAlg ‘ℂfld)‘ℝ)))
2322mptru 1532 . . . . . . . . . . . 12 (Base‘ℂfld) = (Base‘((subringAlg ‘ℂfld)‘ℝ))
2414, 23eqtri 2821 . . . . . . . . . . 11 ℂ = (Base‘((subringAlg ‘ℂfld)‘ℝ))
2524, 18lindssn 30581 . . . . . . . . . 10 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → {1} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
267, 20, 21, 25mp3an 1453 . . . . . . . . 9 {1} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
2726a1i 11 . . . . . . . 8 (⊤ → {1} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
28 ax-icn 10449 . . . . . . . . . 10 i ∈ ℂ
29 ine0 10929 . . . . . . . . . 10 i ≠ 0
3024, 18lindssn 30581 . . . . . . . . . 10 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec ∧ i ∈ ℂ ∧ i ≠ 0) → {i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
317, 28, 29, 30mp3an 1453 . . . . . . . . 9 {i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
3231a1i 11 . . . . . . . 8 (⊤ → {i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
33 lveclmod 19572 . . . . . . . . . . . . . . 15 (((subringAlg ‘ℂfld)‘ℝ) ∈ LVec → ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod)
347, 33ax-mp 5 . . . . . . . . . . . . . 14 ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod
35 df-refld 20435 . . . . . . . . . . . . . . . 16 fld = (ℂflds ℝ)
3610, 16srasca 19647 . . . . . . . . . . . . . . . . 17 (⊤ → (ℂflds ℝ) = (Scalar‘((subringAlg ‘ℂfld)‘ℝ)))
3736mptru 1532 . . . . . . . . . . . . . . . 16 (ℂflds ℝ) = (Scalar‘((subringAlg ‘ℂfld)‘ℝ))
3835, 37eqtri 2821 . . . . . . . . . . . . . . 15 fld = (Scalar‘((subringAlg ‘ℂfld)‘ℝ))
39 cnfldmul 20237 . . . . . . . . . . . . . . . 16 · = (.r‘ℂfld)
4010, 16sravsca 19648 . . . . . . . . . . . . . . . . 17 (⊤ → (.r‘ℂfld) = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ)))
4140mptru 1532 . . . . . . . . . . . . . . . 16 (.r‘ℂfld) = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ))
4239, 41eqtri 2821 . . . . . . . . . . . . . . 15 · = ( ·𝑠 ‘((subringAlg ‘ℂfld)‘ℝ))
4338, 4, 24, 42, 9lspsnel 19469 . . . . . . . . . . . . . 14 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LMod ∧ 1 ∈ ℂ) → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ↔ ∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1)))
4434, 20, 43mp2an 688 . . . . . . . . . . . . 13 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ↔ ∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1))
4538, 4, 24, 42, 9lspsnel 19469 . . . . . . . . . . . . . 14 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LMod ∧ i ∈ ℂ) → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i}) ↔ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
4634, 28, 45mp2an 688 . . . . . . . . . . . . 13 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i}) ↔ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i))
4744, 46anbi12i 626 . . . . . . . . . . . 12 ((𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ (∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1) ∧ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
48 reeanv 3330 . . . . . . . . . . . 12 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1) ∧ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
49 simprl 767 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑥 · 1))
50 simpll 763 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℝ)
5150recnd 10522 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℂ)
5251mulid1d 10511 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑥 · 1) = 𝑥)
5349, 52eqtrd 2833 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 𝑥)
5453negeqd 10733 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑧 = -𝑥)
55 simprr 769 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑦 · i))
56 simplr 765 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℝ)
5756recnd 10522 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℂ)
5828a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → i ∈ ℂ)
5957, 58mulcomd 10515 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑦 · i) = (i · 𝑦))
6055, 59eqtrd 2833 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (i · 𝑦))
6154, 60oveq12d 7041 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = (-𝑥 + (i · 𝑦)))
6253, 51eqeltrd 2885 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 ∈ ℂ)
6362subidd 10839 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑧𝑧) = 0)
6463negeqd 10733 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧𝑧) = -0)
6562, 62negsubdid 10866 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧𝑧) = (-𝑧 + 𝑧))
66 neg0 10786 . . . . . . . . . . . . . . . . . . . . . 22 -0 = 0
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 = 0)
6864, 65, 673eqtr3d 2841 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = 0)
6961, 68eqtr3d 2835 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑥 + (i · 𝑦)) = 0)
7050renegcld 10921 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑥 ∈ ℝ)
71 creq0 30155 . . . . . . . . . . . . . . . . . . . 20 ((-𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((-𝑥 = 0 ∧ 𝑦 = 0) ↔ (-𝑥 + (i · 𝑦)) = 0))
7270, 56, 71syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → ((-𝑥 = 0 ∧ 𝑦 = 0) ↔ (-𝑥 + (i · 𝑦)) = 0))
7369, 72mpbird 258 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑥 = 0 ∧ 𝑦 = 0))
7473simpld 495 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑥 = 0)
7551, 74negcon1ad 10846 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 = 𝑥)
7653, 75, 673eqtr2d 2839 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 0)
7776ex 413 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0))
7877rexlimivv 3257 . . . . . . . . . . . . 13 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0)
79 0red 10497 . . . . . . . . . . . . . 14 (𝑧 = 0 → 0 ∈ ℝ)
80 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 0 ∧ 𝑥 = 0) → 𝑥 = 0)
8180oveq1d 7038 . . . . . . . . . . . . . . . . 17 ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑥 · 1) = (0 · 1))
8281eqeq2d 2807 . . . . . . . . . . . . . . . 16 ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑧 = (𝑥 · 1) ↔ 𝑧 = (0 · 1)))
8382anbi1d 629 . . . . . . . . . . . . . . 15 ((𝑧 = 0 ∧ 𝑥 = 0) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i))))
8483rexbidv 3262 . . . . . . . . . . . . . 14 ((𝑧 = 0 ∧ 𝑥 = 0) → (∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i))))
85 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 0 ∧ 𝑦 = 0) → 𝑦 = 0)
8685oveq1d 7038 . . . . . . . . . . . . . . . . 17 ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑦 · i) = (0 · i))
8786eqeq2d 2807 . . . . . . . . . . . . . . . 16 ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑧 = (𝑦 · i) ↔ 𝑧 = (0 · i)))
8887anbi2d 628 . . . . . . . . . . . . . . 15 ((𝑧 = 0 ∧ 𝑦 = 0) → ((𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i))))
8920mul02i 10682 . . . . . . . . . . . . . . . . . 18 (0 · 1) = 0
9089eqeq2i 2809 . . . . . . . . . . . . . . . . 17 (𝑧 = (0 · 1) ↔ 𝑧 = 0)
9190biimpri 229 . . . . . . . . . . . . . . . 16 (𝑧 = 0 → 𝑧 = (0 · 1))
9228mul02i 10682 . . . . . . . . . . . . . . . . . 18 (0 · i) = 0
9392eqeq2i 2809 . . . . . . . . . . . . . . . . 17 (𝑧 = (0 · i) ↔ 𝑧 = 0)
9493biimpri 229 . . . . . . . . . . . . . . . 16 (𝑧 = 0 → 𝑧 = (0 · i))
9591, 94jca 512 . . . . . . . . . . . . . . 15 (𝑧 = 0 → (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i)))
9679, 88, 95rspcedvd 3568 . . . . . . . . . . . . . 14 (𝑧 = 0 → ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)))
9779, 84, 96rspcedvd 3568 . . . . . . . . . . . . 13 (𝑧 = 0 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)))
9878, 97impbii 210 . . . . . . . . . . . 12 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ 𝑧 = 0)
9947, 48, 983bitr2i 300 . . . . . . . . . . 11 ((𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ 𝑧 = 0)
100 elin 4096 . . . . . . . . . . 11 (𝑧 ∈ (((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})))
101 velsn 4494 . . . . . . . . . . 11 (𝑧 ∈ {0} ↔ 𝑧 = 0)
10299, 100, 1013bitr4i 304 . . . . . . . . . 10 (𝑧 ∈ (((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{i})) ↔ 𝑧 ∈ {0})
103102eqriv 2794 . . . . . . . . 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 30621 . . . . . . 7 (⊤ → ({1} ∪ {i}) ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)))
106105mptru 1532 . . . . . 6 ({1} ∪ {i}) ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
1078, 106eqeltri 2881 . . . . 5 {1, i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ))
108 cnfldadd 20236 . . . . . . . . . 10 + = (+g‘ℂfld)
10910, 16sraaddg 19645 . . . . . . . . . . 11 (⊤ → (+g‘ℂfld) = (+g‘((subringAlg ‘ℂfld)‘ℝ)))
110109mptru 1532 . . . . . . . . . 10 (+g‘ℂfld) = (+g‘((subringAlg ‘ℂfld)‘ℝ))
111108, 110eqtri 2821 . . . . . . . . 9 + = (+g‘((subringAlg ‘ℂfld)‘ℝ))
11234a1i 11 . . . . . . . . 9 (⊤ → ((subringAlg ‘ℂfld)‘ℝ) ∈ LMod)
113 1cnd 10489 . . . . . . . . 9 (⊤ → 1 ∈ ℂ)
11428a1i 11 . . . . . . . . 9 (⊤ → i ∈ ℂ)
11524, 111, 38, 4, 42, 9, 112, 113, 114lspprel 19560 . . . . . . . 8 (⊤ → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i))))
116115mptru 1532 . . . . . . 7 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)))
117 simpl 483 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ)
118117recnd 10522 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℂ)
119 1cnd 10489 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
120118, 119mulcld 10514 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 1) ∈ ℂ)
121 simpr 485 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
122121recnd 10522 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
12328a1i 11 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → i ∈ ℂ)
124122, 123mulcld 10514 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · i) ∈ ℂ)
125120, 124addcld 10513 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + (𝑦 · i)) ∈ ℂ)
126 eleq1 2872 . . . . . . . . . 10 (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → (𝑧 ∈ ℂ ↔ ((𝑥 · 1) + (𝑦 · i)) ∈ ℂ))
127125, 126syl5ibrcom 248 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈ ℂ))
128127rexlimivv 3257 . . . . . . . 8 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈ ℂ)
129 recl 14307 . . . . . . . . 9 (𝑧 ∈ ℂ → (ℜ‘𝑧) ∈ ℝ)
130 simpr 485 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → 𝑥 = (ℜ‘𝑧))
131130oveq1d 7038 . . . . . . . . . . . 12 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑥 · 1) = ((ℜ‘𝑧) · 1))
132131oveq1d 7038 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → ((𝑥 · 1) + (𝑦 · i)) = (((ℜ‘𝑧) · 1) + (𝑦 · i)))
133132eqeq2d 2807 . . . . . . . . . 10 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i))))
134133rexbidv 3262 . . . . . . . . 9 ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i))))
135 imcl 14308 . . . . . . . . . 10 (𝑧 ∈ ℂ → (ℑ‘𝑧) ∈ ℝ)
136 simpr 485 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → 𝑦 = (ℑ‘𝑧))
137136oveq1d 7038 . . . . . . . . . . . 12 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑦 · i) = ((ℑ‘𝑧) · i))
138137oveq2d 7039 . . . . . . . . . . 11 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (((ℜ‘𝑧) · 1) + (𝑦 · i)) = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)))
139138eqeq2d 2807 . . . . . . . . . 10 ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i))))
140 replim 14313 . . . . . . . . . . 11 (𝑧 ∈ ℂ → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
141129recnd 10522 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → (ℜ‘𝑧) ∈ ℂ)
142141mulid1d 10511 . . . . . . . . . . . 12 (𝑧 ∈ ℂ → ((ℜ‘𝑧) · 1) = (ℜ‘𝑧))
143135recnd 10522 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → (ℑ‘𝑧) ∈ ℂ)
14428a1i 11 . . . . . . . . . . . . 13 (𝑧 ∈ ℂ → i ∈ ℂ)
145143, 144mulcomd 10515 . . . . . . . . . . . 12 (𝑧 ∈ ℂ → ((ℑ‘𝑧) · i) = (i · (ℑ‘𝑧)))
146142, 145oveq12d 7041 . . . . . . . . . . 11 (𝑧 ∈ ℂ → (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)) = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
147140, 146eqtr4d 2836 . . . . . . . . . 10 (𝑧 ∈ ℂ → 𝑧 = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)))
148135, 139, 147rspcedvd 3568 . . . . . . . . 9 (𝑧 ∈ ℂ → ∃𝑦 ∈ ℝ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)))
149129, 134, 148rspcedvd 3568 . . . . . . . 8 (𝑧 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)))
150128, 149impbii 210 . . . . . . 7 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 ∈ ℂ)
151116, 150bitri 276 . . . . . 6 (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) ↔ 𝑧 ∈ ℂ)
152151eqriv 2794 . . . . 5 ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) = ℂ
153 eqid 2797 . . . . . 6 (LBasis‘((subringAlg ‘ℂfld)‘ℝ)) = (LBasis‘((subringAlg ‘ℂfld)‘ℝ))
15424, 153, 9islbs4 20662 . . . . 5 ({1, i} ∈ (LBasis‘((subringAlg ‘ℂfld)‘ℝ)) ↔ ({1, i} ∈ (LIndS‘((subringAlg ‘ℂfld)‘ℝ)) ∧ ((LSpan‘((subringAlg ‘ℂfld)‘ℝ))‘{1, i}) = ℂ))
155107, 152, 154mpbir2an 707 . . . 4 {1, i} ∈ (LBasis‘((subringAlg ‘ℂfld)‘ℝ))
156153dimval 30601 . . . 4 ((((subringAlg ‘ℂfld)‘ℝ) ∈ LVec ∧ {1, i} ∈ (LBasis‘((subringAlg ‘ℂfld)‘ℝ))) → (dim‘((subringAlg ‘ℂfld)‘ℝ)) = (♯‘{1, i}))
1577, 155, 156mp2an 688 . . 3 (dim‘((subringAlg ‘ℂfld)‘ℝ)) = (♯‘{1, i})
158 1nei 30156 . . . 4 1 ≠ i
159 hashprg 13608 . . . . 5 ((1 ∈ ℂ ∧ i ∈ ℂ) → (1 ≠ i ↔ (♯‘{1, i}) = 2))
16020, 28, 159mp2an 688 . . . 4 (1 ≠ i ↔ (♯‘{1, i}) = 2)
161158, 160mpbi 231 . . 3 (♯‘{1, i}) = 2
162157, 161eqtri 2821 . 2 (dim‘((subringAlg ‘ℂfld)‘ℝ)) = 2
1633, 6, 1623eqtr2i 2827 1 (ℂfld[:]ℝfld) = 2
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1525  wtru 1526  wcel 2083  wne 2986  wrex 3108  cun 3863  cin 3864  wss 3865  {csn 4478  {cpr 4480   class class class wbr 4968  cfv 6232  (class class class)co 7023  cc 10388  cr 10389  0cc0 10390  1c1 10391  ici 10392   + caddc 10393   · cmul 10395  cmin 10723  -cneg 10724  2c2 11546  chash 13544  cre 14294  cim 14295  Basecbs 16316  s cress 16317  +gcplusg 16398  .rcmulr 16399  Scalarcsca 16401   ·𝑠 cvsca 16402  0gc0g 16546  LModclmod 19328  LSpanclspn 19437  LBasisclbs 19540  LVecclvec 19568  subringAlg csra 19634  fldccnfld 20231  fldcrefld 20434  LIndSclinds 20635  dimcldim 30599  /FldExtcfldext 30628  [:]cextdg 30631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-reg 8909  ax-inf2 8957  ax-ac2 9738  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-addf 10469  ax-mulf 10470
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-fal 1538  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-iin 4834  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-tpos 7750  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-oadd 7964  df-er 8146  df-map 8265  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-oi 8827  df-r1 9046  df-rank 9047  df-dju 9183  df-card 9221  df-acn 9224  df-ac 9395  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-4 11556  df-5 11557  df-6 11558  df-7 11559  df-8 11560  df-9 11561  df-n0 11752  df-xnn0 11822  df-z 11836  df-dec 11953  df-uz 12098  df-fz 12747  df-hash 13545  df-cj 14296  df-re 14297  df-im 14298  df-struct 16318  df-ndx 16319  df-slot 16320  df-base 16322  df-sets 16323  df-ress 16324  df-plusg 16411  df-mulr 16412  df-starv 16413  df-sca 16414  df-vsca 16415  df-ip 16416  df-tset 16417  df-ple 16418  df-ocomp 16419  df-ds 16420  df-unif 16421  df-0g 16548  df-mre 16690  df-mrc 16691  df-mri 16692  df-acs 16693  df-proset 17371  df-drs 17372  df-poset 17389  df-ipo 17595  df-mgm 17685  df-sgrp 17727  df-mnd 17738  df-submnd 17779  df-grp 17868  df-minusg 17869  df-sbg 17870  df-subg 18034  df-cntz 18192  df-lsm 18495  df-cmn 18639  df-abl 18640  df-mgp 18934  df-ur 18946  df-ring 18993  df-cring 18994  df-oppr 19067  df-dvdsr 19085  df-unit 19086  df-invr 19116  df-dvr 19127  df-drng 19198  df-field 19199  df-subrg 19227  df-lmod 19330  df-lss 19398  df-lsp 19438  df-lbs 19541  df-lvec 19569  df-sra 19638  df-cnfld 20232  df-refld 20435  df-lindf 20636  df-linds 20637  df-dim 30600  df-fldext 30632  df-extdg 30633
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator