Metamath Proof Explorer

Theorem ccfldextdgrr

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)

Ref Expression
Assertion ccfldextdgrr ( ℂfld [:] ℝfld ) = 2

Proof

Step Hyp Ref Expression
1 ccfldextrr ⊢ ℂfld /FldExt ℝfld
2 extdgval ⊢ ( ℂfld /FldExt ℝfld → ( ℂfld [:] ℝfld ) = ( dim ‘ ( ( subringAlg ‘ ℂfld ) ‘ ( Base ‘ ℝfld ) ) ) )
3 1 2 ax-mp ⊢ ( ℂfld [:] ℝfld ) = ( dim ‘ ( ( subringAlg ‘ ℂfld ) ‘ ( Base ‘ ℝfld ) ) )
4 rebase ⊢ ℝ = ( Base ‘ ℝfld )
5 4 fveq2i ⊢ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) = ( ( subringAlg ‘ ℂfld ) ‘ ( Base ‘ ℝfld ) )
6 5 fveq2i ⊢ ( dim ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) = ( dim ‘ ( ( subringAlg ‘ ℂfld ) ‘ ( Base ‘ ℝfld ) ) )
7 ccfldsrarelvec ⊢ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LVec
8 df-pr ⊢ { 1 , i } = ( { 1 } ∪ { i } )
9 eqid ⊢ ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) = ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
10 eqidd ⊢ ( ⊤ → ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) = ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
11 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
12 11 a1i ⊢ ( ⊤ → 0 = ( 0g ‘ ℂfld ) )
13 ax-resscn ⊢ ℝ ⊆ ℂ
14 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
15 13 14 sseqtri ⊢ ℝ ⊆ ( Base ‘ ℂfld )
16 15 a1i ⊢ ( ⊤ → ℝ ⊆ ( Base ‘ ℂfld ) )
17 10 12 16 sralmod0 ⊢ ( ⊤ → 0 = ( 0g ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
18 17 mptru ⊢ 0 = ( 0g ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
19 7 a1i ⊢ ( ⊤ → ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LVec )
20 ax-1cn ⊢ 1 ∈ ℂ
21 ax-1ne0 ⊢ 1 ≠ 0
22 10 16 srabase ⊢ ( ⊤ → ( Base ‘ ℂfld ) = ( Base ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
23 22 mptru ⊢ ( Base ‘ ℂfld ) = ( Base ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
24 14 23 eqtri ⊢ ℂ = ( Base ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
25 24 18 lindssn ⊢ ( ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LVec ∧ 1 ∈ ℂ ∧ 1 ≠ 0 ) → { 1 } ∈ ( LIndS ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
26 7 20 21 25 mp3an ⊢ { 1 } ∈ ( LIndS ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
27 26 a1i ⊢ ( ⊤ → { 1 } ∈ ( LIndS ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
28 ax-icn ⊢ i ∈ ℂ
29 ine0 ⊢ i ≠ 0
30 24 18 lindssn ⊢ ( ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LVec ∧ i ∈ ℂ ∧ i ≠ 0 ) → { i } ∈ ( LIndS ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
31 7 28 29 30 mp3an ⊢ { i } ∈ ( LIndS ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
32 31 a1i ⊢ ( ⊤ → { i } ∈ ( LIndS ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
33 lveclmod ⊢ ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LVec → ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LMod )
34 7 33 ax-mp ⊢ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LMod
35 df-refld ⊢ ℝfld = ( ℂfld ↾s ℝ )
36 10 16 srasca ⊢ ( ⊤ → ( ℂfld ↾s ℝ ) = ( Scalar ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
37 36 mptru ⊢ ( ℂfld ↾s ℝ ) = ( Scalar ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
38 35 37 eqtri ⊢ ℝfld = ( Scalar ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
39 cnfldmul ⊢ · = ( .r ‘ ℂfld )
40 10 16 sravsca ⊢ ( ⊤ → ( .r ‘ ℂfld ) = ( ·𝑠 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
41 40 mptru ⊢ ( .r ‘ ℂfld ) = ( ·𝑠 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
42 39 41 eqtri ⊢ · = ( ·𝑠 ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
43 38 4 24 42 9 ellspsn ⊢ ( ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LMod ∧ 1 ∈ ℂ ) → ( 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 } ) ↔ ∃ 𝑥 ∈ ℝ 𝑧 = ( 𝑥 · 1 ) ) )
44 34 20 43 mp2an ⊢ ( 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 } ) ↔ ∃ 𝑥 ∈ ℝ 𝑧 = ( 𝑥 · 1 ) )
45 38 4 24 42 9 ellspsn ⊢ ( ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LMod ∧ i ∈ ℂ ) → ( 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { i } ) ↔ ∃ 𝑦 ∈ ℝ 𝑧 = ( 𝑦 · i ) ) )
46 34 28 45 mp2an ⊢ ( 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { i } ) ↔ ∃ 𝑦 ∈ ℝ 𝑧 = ( 𝑦 · i ) )
47 44 46 anbi12i ⊢ ( ( 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 } ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { i } ) ) ↔ ( ∃ 𝑥 ∈ ℝ 𝑧 = ( 𝑥 · 1 ) ∧ ∃ 𝑦 ∈ ℝ 𝑧 = ( 𝑦 · i ) ) )
48 reeanv ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ↔ ( ∃ 𝑥 ∈ ℝ 𝑧 = ( 𝑥 · 1 ) ∧ ∃ 𝑦 ∈ ℝ 𝑧 = ( 𝑦 · i ) ) )
49 simprl ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → 𝑧 = ( 𝑥 · 1 ) )
50 simpll ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → 𝑥 ∈ ℝ )
51 50 recnd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → 𝑥 ∈ ℂ )
52 51 mulridd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → ( 𝑥 · 1 ) = 𝑥 )
53 49 52 eqtrd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → 𝑧 = 𝑥 )
54 53 negeqd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → - 𝑧 = - 𝑥 )
55 simprr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → 𝑧 = ( 𝑦 · i ) )
56 simplr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → 𝑦 ∈ ℝ )
57 56 recnd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → 𝑦 ∈ ℂ )
58 28 a1i ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → i ∈ ℂ )
59 57 58 mulcomd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → ( 𝑦 · i ) = ( i · 𝑦 ) )
60 55 59 eqtrd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → 𝑧 = ( i · 𝑦 ) )
61 54 60 oveq12d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → ( - 𝑧 + 𝑧 ) = ( - 𝑥 + ( i · 𝑦 ) ) )
62 53 51 eqeltrd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → 𝑧 ∈ ℂ )
63 62 subidd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → ( 𝑧 − 𝑧 ) = 0 )
64 63 negeqd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → - ( 𝑧 − 𝑧 ) = - 0 )
65 62 62 negsubdid ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → - ( 𝑧 − 𝑧 ) = ( - 𝑧 + 𝑧 ) )
66 neg0 ⊢ - 0 = 0
67 66 a1i ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → - 0 = 0 )
68 64 65 67 3eqtr3d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → ( - 𝑧 + 𝑧 ) = 0 )
69 61 68 eqtr3d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → ( - 𝑥 + ( i · 𝑦 ) ) = 0 )
70 50 renegcld ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → - 𝑥 ∈ ℝ )
71 creq0 ⊢ ( ( - 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( - 𝑥 = 0 ∧ 𝑦 = 0 ) ↔ ( - 𝑥 + ( i · 𝑦 ) ) = 0 ) )
72 70 56 71 syl2anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → ( ( - 𝑥 = 0 ∧ 𝑦 = 0 ) ↔ ( - 𝑥 + ( i · 𝑦 ) ) = 0 ) )
73 69 72 mpbird ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → ( - 𝑥 = 0 ∧ 𝑦 = 0 ) )
74 73 simpld ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → - 𝑥 = 0 )
75 51 74 negcon1ad ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → - 0 = 𝑥 )
76 53 75 67 3eqtr2d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) → 𝑧 = 0 )
77 76 ex ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) → 𝑧 = 0 ) )
78 77 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) → 𝑧 = 0 )
79 0red ⊢ ( 𝑧 = 0 → 0 ∈ ℝ )
80 simpr ⊢ ( ( 𝑧 = 0 ∧ 𝑥 = 0 ) → 𝑥 = 0 )
81 80 oveq1d ⊢ ( ( 𝑧 = 0 ∧ 𝑥 = 0 ) → ( 𝑥 · 1 ) = ( 0 · 1 ) )
82 81 eqeq2d ⊢ ( ( 𝑧 = 0 ∧ 𝑥 = 0 ) → ( 𝑧 = ( 𝑥 · 1 ) ↔ 𝑧 = ( 0 · 1 ) ) )
83 82 anbi1d ⊢ ( ( 𝑧 = 0 ∧ 𝑥 = 0 ) → ( ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ↔ ( 𝑧 = ( 0 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) )
84 83 rexbidv ⊢ ( ( 𝑧 = 0 ∧ 𝑥 = 0 ) → ( ∃ 𝑦 ∈ ℝ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ↔ ∃ 𝑦 ∈ ℝ ( 𝑧 = ( 0 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ) )
85 simpr ⊢ ( ( 𝑧 = 0 ∧ 𝑦 = 0 ) → 𝑦 = 0 )
86 85 oveq1d ⊢ ( ( 𝑧 = 0 ∧ 𝑦 = 0 ) → ( 𝑦 · i ) = ( 0 · i ) )
87 86 eqeq2d ⊢ ( ( 𝑧 = 0 ∧ 𝑦 = 0 ) → ( 𝑧 = ( 𝑦 · i ) ↔ 𝑧 = ( 0 · i ) ) )
88 87 anbi2d ⊢ ( ( 𝑧 = 0 ∧ 𝑦 = 0 ) → ( ( 𝑧 = ( 0 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ↔ ( 𝑧 = ( 0 · 1 ) ∧ 𝑧 = ( 0 · i ) ) ) )
89 20 mul02i ⊢ ( 0 · 1 ) = 0
90 89 eqeq2i ⊢ ( 𝑧 = ( 0 · 1 ) ↔ 𝑧 = 0 )
91 90 biimpri ⊢ ( 𝑧 = 0 → 𝑧 = ( 0 · 1 ) )
92 28 mul02i ⊢ ( 0 · i ) = 0
93 92 eqeq2i ⊢ ( 𝑧 = ( 0 · i ) ↔ 𝑧 = 0 )
94 93 biimpri ⊢ ( 𝑧 = 0 → 𝑧 = ( 0 · i ) )
95 91 94 jca ⊢ ( 𝑧 = 0 → ( 𝑧 = ( 0 · 1 ) ∧ 𝑧 = ( 0 · i ) ) )
96 79 88 95 rspcedvd ⊢ ( 𝑧 = 0 → ∃ 𝑦 ∈ ℝ ( 𝑧 = ( 0 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) )
97 79 84 96 rspcedvd ⊢ ( 𝑧 = 0 → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) )
98 78 97 impbii ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( 𝑧 = ( 𝑥 · 1 ) ∧ 𝑧 = ( 𝑦 · i ) ) ↔ 𝑧 = 0 )
99 47 48 98 3bitr2i ⊢ ( ( 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 } ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { i } ) ) ↔ 𝑧 = 0 )
100 elin ⊢ ( 𝑧 ∈ ( ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 } ) ∩ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { i } ) ) ↔ ( 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 } ) ∧ 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { i } ) ) )
101 velsn ⊢ ( 𝑧 ∈ { 0 } ↔ 𝑧 = 0 )
102 99 100 101 3bitr4i ⊢ ( 𝑧 ∈ ( ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 } ) ∩ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { i } ) ) ↔ 𝑧 ∈ { 0 } )
103 102 eqriv ⊢ ( ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 } ) ∩ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { i } ) ) = { 0 }
104 103 a1i ⊢ ( ⊤ → ( ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 } ) ∩ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { i } ) ) = { 0 } )
105 9 18 19 27 32 104 lindsun ⊢ ( ⊤ → ( { 1 } ∪ { i } ) ∈ ( LIndS ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
106 105 mptru ⊢ ( { 1 } ∪ { i } ) ∈ ( LIndS ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
107 8 106 eqeltri ⊢ { 1 , i } ∈ ( LIndS ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
108 cnfldadd ⊢ + = ( +g ‘ ℂfld )
109 10 16 sraaddg ⊢ ( ⊤ → ( +g ‘ ℂfld ) = ( +g ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) )
110 109 mptru ⊢ ( +g ‘ ℂfld ) = ( +g ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
111 108 110 eqtri ⊢ + = ( +g ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
112 34 a1i ⊢ ( ⊤ → ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LMod )
113 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
114 28 a1i ⊢ ( ⊤ → i ∈ ℂ )
115 24 111 38 4 42 9 112 113 114 lspprel ⊢ ( ⊤ → ( 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 , i } ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑧 = ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) ) )
116 115 mptru ⊢ ( 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 , i } ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑧 = ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) )
117 simpl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℝ )
118 117 recnd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℂ )
119 1cnd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℂ )
120 118 119 mulcld ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 1 ) ∈ ℂ )
121 simpr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
122 121 recnd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
123 28 a1i ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → i ∈ ℂ )
124 122 123 mulcld ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑦 · i ) ∈ ℂ )
125 120 124 addcld ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) ∈ ℂ )
126 eleq1 ⊢ ( 𝑧 = ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) → ( 𝑧 ∈ ℂ ↔ ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) ∈ ℂ ) )
127 125 126 syl5ibrcom ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 = ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) → 𝑧 ∈ ℂ ) )
128 127 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑧 = ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) → 𝑧 ∈ ℂ )
129 recl ⊢ ( 𝑧 ∈ ℂ → ( ℜ ‘ 𝑧 ) ∈ ℝ )
130 simpr ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 = ( ℜ ‘ 𝑧 ) ) → 𝑥 = ( ℜ ‘ 𝑧 ) )
131 130 oveq1d ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 = ( ℜ ‘ 𝑧 ) ) → ( 𝑥 · 1 ) = ( ( ℜ ‘ 𝑧 ) · 1 ) )
132 131 oveq1d ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 = ( ℜ ‘ 𝑧 ) ) → ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) = ( ( ( ℜ ‘ 𝑧 ) · 1 ) + ( 𝑦 · i ) ) )
133 132 eqeq2d ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 = ( ℜ ‘ 𝑧 ) ) → ( 𝑧 = ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) ↔ 𝑧 = ( ( ( ℜ ‘ 𝑧 ) · 1 ) + ( 𝑦 · i ) ) ) )
134 133 rexbidv ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 = ( ℜ ‘ 𝑧 ) ) → ( ∃ 𝑦 ∈ ℝ 𝑧 = ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) ↔ ∃ 𝑦 ∈ ℝ 𝑧 = ( ( ( ℜ ‘ 𝑧 ) · 1 ) + ( 𝑦 · i ) ) ) )
135 imcl ⊢ ( 𝑧 ∈ ℂ → ( ℑ ‘ 𝑧 ) ∈ ℝ )
136 simpr ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑦 = ( ℑ ‘ 𝑧 ) ) → 𝑦 = ( ℑ ‘ 𝑧 ) )
137 136 oveq1d ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑦 = ( ℑ ‘ 𝑧 ) ) → ( 𝑦 · i ) = ( ( ℑ ‘ 𝑧 ) · i ) )
138 137 oveq2d ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑦 = ( ℑ ‘ 𝑧 ) ) → ( ( ( ℜ ‘ 𝑧 ) · 1 ) + ( 𝑦 · i ) ) = ( ( ( ℜ ‘ 𝑧 ) · 1 ) + ( ( ℑ ‘ 𝑧 ) · i ) ) )
139 138 eqeq2d ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑦 = ( ℑ ‘ 𝑧 ) ) → ( 𝑧 = ( ( ( ℜ ‘ 𝑧 ) · 1 ) + ( 𝑦 · i ) ) ↔ 𝑧 = ( ( ( ℜ ‘ 𝑧 ) · 1 ) + ( ( ℑ ‘ 𝑧 ) · i ) ) ) )
140 replim ⊢ ( 𝑧 ∈ ℂ → 𝑧 = ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) )
141 129 recnd ⊢ ( 𝑧 ∈ ℂ → ( ℜ ‘ 𝑧 ) ∈ ℂ )
142 141 mulridd ⊢ ( 𝑧 ∈ ℂ → ( ( ℜ ‘ 𝑧 ) · 1 ) = ( ℜ ‘ 𝑧 ) )
143 135 recnd ⊢ ( 𝑧 ∈ ℂ → ( ℑ ‘ 𝑧 ) ∈ ℂ )
144 28 a1i ⊢ ( 𝑧 ∈ ℂ → i ∈ ℂ )
145 143 144 mulcomd ⊢ ( 𝑧 ∈ ℂ → ( ( ℑ ‘ 𝑧 ) · i ) = ( i · ( ℑ ‘ 𝑧 ) ) )
146 142 145 oveq12d ⊢ ( 𝑧 ∈ ℂ → ( ( ( ℜ ‘ 𝑧 ) · 1 ) + ( ( ℑ ‘ 𝑧 ) · i ) ) = ( ( ℜ ‘ 𝑧 ) + ( i · ( ℑ ‘ 𝑧 ) ) ) )
147 140 146 eqtr4d ⊢ ( 𝑧 ∈ ℂ → 𝑧 = ( ( ( ℜ ‘ 𝑧 ) · 1 ) + ( ( ℑ ‘ 𝑧 ) · i ) ) )
148 135 139 147 rspcedvd ⊢ ( 𝑧 ∈ ℂ → ∃ 𝑦 ∈ ℝ 𝑧 = ( ( ( ℜ ‘ 𝑧 ) · 1 ) + ( 𝑦 · i ) ) )
149 129 134 148 rspcedvd ⊢ ( 𝑧 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑧 = ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) )
150 128 149 impbii ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑧 = ( ( 𝑥 · 1 ) + ( 𝑦 · i ) ) ↔ 𝑧 ∈ ℂ )
151 116 150 bitri ⊢ ( 𝑧 ∈ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 , i } ) ↔ 𝑧 ∈ ℂ )
152 151 eqriv ⊢ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 , i } ) = ℂ
153 eqid ⊢ ( LBasis ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) = ( LBasis ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
154 24 153 9 islbs4 ⊢ ( { 1 , i } ∈ ( LBasis ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ↔ ( { 1 , i } ∈ ( LIndS ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ∧ ( ( LSpan ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ‘ { 1 , i } ) = ℂ ) )
155 107 152 154 mpbir2an ⊢ { 1 , i } ∈ ( LBasis ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) )
156 153 dimval ⊢ ( ( ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ∈ LVec ∧ { 1 , i } ∈ ( LBasis ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) ) → ( dim ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) = ( ♯ ‘ { 1 , i } ) )
157 7 155 156 mp2an ⊢ ( dim ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) = ( ♯ ‘ { 1 , i } )
158 1nei ⊢ 1 ≠ i
159 hashprg ⊢ ( ( 1 ∈ ℂ ∧ i ∈ ℂ ) → ( 1 ≠ i ↔ ( ♯ ‘ { 1 , i } ) = 2 ) )
160 20 28 159 mp2an ⊢ ( 1 ≠ i ↔ ( ♯ ‘ { 1 , i } ) = 2 )
161 158 160 mpbi ⊢ ( ♯ ‘ { 1 , i } ) = 2
162 157 161 eqtri ⊢ ( dim ‘ ( ( subringAlg ‘ ℂfld ) ‘ ℝ ) ) = 2
163 3 6 162 3eqtr2i ⊢ ( ℂfld [:] ℝfld ) = 2