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

Metamath Proof Explorer

Theorem ccfldextdgrr

Proof