This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( CCfld [:] RRfld ) = 2

Proof

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