ccfldextdgrr - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ccfldextdgrr		Structured version Visualization version GIF version

Theorem ccfldextdgrr 33837

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.

Step	Hyp	Ref	Expression
1		ccfldextrr 33811	. . 3 ⊢ ℂ_fld/_FldExtℝ_fld
2		extdgval 33818	. . 3 ⊢ (ℂ_fld/_FldExtℝ_fld → (ℂ_fld[:]ℝ_fld) = (dim‘((subringAlg ‘ℂ_fld)‘(Base‘ℝ_fld))))
3	1, 2	ax-mp 5	. 2 ⊢ (ℂ_fld[:]ℝ_fld) = (dim‘((subringAlg ‘ℂ_fld)‘(Base‘ℝ_fld)))
4		rebase 21594	. . . 4 ⊢ ℝ = (Base‘ℝ_fld)
5	4	fveq2i 6835	. . 3 ⊢ ((subringAlg ‘ℂ_fld)‘ℝ) = ((subringAlg ‘ℂ_fld)‘(Base‘ℝ_fld))
6	5	fveq2i 6835	. 2 ⊢ (dim‘((subringAlg ‘ℂ_fld)‘ℝ)) = (dim‘((subringAlg ‘ℂ_fld)‘(Base‘ℝ_fld)))
7		ccfldsrarelvec 33836	. . . 4 ⊢ ((subringAlg ‘ℂ_fld)‘ℝ) ∈ LVec
8		df-pr 4571	. . . . . 6 ⊢ {1, i} = ({1} ∪ {i})
9		eqid 2737	. . . . . . . 8 ⊢ (LSpan‘((subringAlg ‘ℂ_fld)‘ℝ)) = (LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))
10		eqidd 2738	. . . . . . . . . 10 ⊢ (⊤ → ((subringAlg ‘ℂ_fld)‘ℝ) = ((subringAlg ‘ℂ_fld)‘ℝ))
11		cnfld0 21380	. . . . . . . . . . 11 ⊢ 0 = (0_g‘ℂ_fld)
12	11	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → 0 = (0_g‘ℂ_fld))
13		ax-resscn 11084	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℂ
14		cnfldbas 21346	. . . . . . . . . . . 12 ⊢ ℂ = (Base‘ℂ_fld)
15	13, 14	sseqtri 3971	. . . . . . . . . . 11 ⊢ ℝ ⊆ (Base‘ℂ_fld)
16	15	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → ℝ ⊆ (Base‘ℂ_fld))
17	10, 12, 16	sralmod0 21173	. . . . . . . . 9 ⊢ (⊤ → 0 = (0_g‘((subringAlg ‘ℂ_fld)‘ℝ)))
18	17	mptru 1549	. . . . . . . 8 ⊢ 0 = (0_g‘((subringAlg ‘ℂ_fld)‘ℝ))
19	7	a1i 11	. . . . . . . 8 ⊢ (⊤ → ((subringAlg ‘ℂ_fld)‘ℝ) ∈ LVec)
20		ax-1cn 11085	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
21		ax-1ne0 11096	. . . . . . . . . 10 ⊢ 1 ≠ 0
22	10, 16	srabase 21162	. . . . . . . . . . . . 13 ⊢ (⊤ → (Base‘ℂ_fld) = (Base‘((subringAlg ‘ℂ_fld)‘ℝ)))
23	22	mptru 1549	. . . . . . . . . . . 12 ⊢ (Base‘ℂ_fld) = (Base‘((subringAlg ‘ℂ_fld)‘ℝ))
24	14, 23	eqtri 2760	. . . . . . . . . . 11 ⊢ ℂ = (Base‘((subringAlg ‘ℂ_fld)‘ℝ))
25	24, 18	lindssn 33458	. . . . . . . . . 10 ⊢ ((((subringAlg ‘ℂ_fld)‘ℝ) ∈ LVec ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → {1} ∈ (LIndS‘((subringAlg ‘ℂ_fld)‘ℝ)))
26	7, 20, 21, 25	mp3an 1464	. . . . . . . . 9 ⊢ {1} ∈ (LIndS‘((subringAlg ‘ℂ_fld)‘ℝ))
27	26	a1i 11	. . . . . . . 8 ⊢ (⊤ → {1} ∈ (LIndS‘((subringAlg ‘ℂ_fld)‘ℝ)))
28		ax-icn 11086	. . . . . . . . . 10 ⊢ i ∈ ℂ
29		ine0 11574	. . . . . . . . . 10 ⊢ i ≠ 0
30	24, 18	lindssn 33458	. . . . . . . . . 10 ⊢ ((((subringAlg ‘ℂ_fld)‘ℝ) ∈ LVec ∧ i ∈ ℂ ∧ i ≠ 0) → {i} ∈ (LIndS‘((subringAlg ‘ℂ_fld)‘ℝ)))
31	7, 28, 29, 30	mp3an 1464	. . . . . . . . 9 ⊢ {i} ∈ (LIndS‘((subringAlg ‘ℂ_fld)‘ℝ))
32	31	a1i 11	. . . . . . . 8 ⊢ (⊤ → {i} ∈ (LIndS‘((subringAlg ‘ℂ_fld)‘ℝ)))
33		lveclmod 21091	. . . . . . . . . . . . . . 15 ⊢ (((subringAlg ‘ℂ_fld)‘ℝ) ∈ LVec → ((subringAlg ‘ℂ_fld)‘ℝ) ∈ LMod)
34	7, 33	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((subringAlg ‘ℂ_fld)‘ℝ) ∈ LMod
35		df-refld 21593	. . . . . . . . . . . . . . . 16 ⊢ ℝ_fld = (ℂ_fld ↾_s ℝ)
36	10, 16	srasca 21165	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (ℂ_fld ↾_s ℝ) = (Scalar‘((subringAlg ‘ℂ_fld)‘ℝ)))
37	36	mptru 1549	. . . . . . . . . . . . . . . 16 ⊢ (ℂ_fld ↾_s ℝ) = (Scalar‘((subringAlg ‘ℂ_fld)‘ℝ))
38	35, 37	eqtri 2760	. . . . . . . . . . . . . . 15 ⊢ ℝ_fld = (Scalar‘((subringAlg ‘ℂ_fld)‘ℝ))
39		cnfldmul 21350	. . . . . . . . . . . . . . . 16 ⊢ · = (._r‘ℂ_fld)
40	10, 16	sravsca 21166	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (._r‘ℂ_fld) = ( ·_𝑠 ‘((subringAlg ‘ℂ_fld)‘ℝ)))
41	40	mptru 1549	. . . . . . . . . . . . . . . 16 ⊢ (._r‘ℂ_fld) = ( ·_𝑠 ‘((subringAlg ‘ℂ_fld)‘ℝ))
42	39, 41	eqtri 2760	. . . . . . . . . . . . . . 15 ⊢ · = ( ·_𝑠 ‘((subringAlg ‘ℂ_fld)‘ℝ))
43	38, 4, 24, 42, 9	ellspsn 20987	. . . . . . . . . . . . . 14 ⊢ ((((subringAlg ‘ℂ_fld)‘ℝ) ∈ LMod ∧ 1 ∈ ℂ) → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1}) ↔ ∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1)))
44	34, 20, 43	mp2an 693	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1}) ↔ ∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1))
45	38, 4, 24, 42, 9	ellspsn 20987	. . . . . . . . . . . . . 14 ⊢ ((((subringAlg ‘ℂ_fld)‘ℝ) ∈ LMod ∧ i ∈ ℂ) → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{i}) ↔ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
46	34, 28, 45	mp2an 693	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{i}) ↔ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i))
47	44, 46	anbi12i 629	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{i})) ↔ (∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1) ∧ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
48		reeanv 3210	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (∃𝑥 ∈ ℝ 𝑧 = (𝑥 · 1) ∧ ∃𝑦 ∈ ℝ 𝑧 = (𝑦 · i)))
49		simprl 771	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑥 · 1))
50		simpll 767	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℝ)
51	50	recnd 11162	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑥 ∈ ℂ)
52	51	mulridd 11151	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑥 · 1) = 𝑥)
53	49, 52	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 𝑥)
54	53	negeqd 11376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑧 = -𝑥)
55		simprr 773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (𝑦 · i))
56		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℝ)
57	56	recnd 11162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑦 ∈ ℂ)
58	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → i ∈ ℂ)
59	57, 58	mulcomd 11155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑦 · i) = (i · 𝑦))
60	55, 59	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = (i · 𝑦))
61	54, 60	oveq12d 7376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = (-𝑥 + (i · 𝑦)))
62	53, 51	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 ∈ ℂ)
63	62	subidd 11482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (𝑧 − 𝑧) = 0)
64	63	negeqd 11376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧 − 𝑧) = -0)
65	62, 62	negsubdid 11509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -(𝑧 − 𝑧) = (-𝑧 + 𝑧))
66		neg0 11429	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -0 = 0
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 = 0)
68	64, 65, 67	3eqtr3d 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑧 + 𝑧) = 0)
69	61, 68	eqtr3d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑥 + (i · 𝑦)) = 0)
70	50	renegcld 11566	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑥 ∈ ℝ)
71		creq0 32829	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((-𝑥 = 0 ∧ 𝑦 = 0) ↔ (-𝑥 + (i · 𝑦)) = 0))
72	70, 56, 71	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → ((-𝑥 = 0 ∧ 𝑦 = 0) ↔ (-𝑥 + (i · 𝑦)) = 0))
73	69, 72	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → (-𝑥 = 0 ∧ 𝑦 = 0))
74	73	simpld 494	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -𝑥 = 0)
75	51, 74	negcon1ad 11489	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → -0 = 𝑥)
76	53, 75, 67	3eqtr2d 2778	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i))) → 𝑧 = 0)
77	76	ex 412	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0))
78	77	rexlimivv 3180	. . . . . . . . . . . . 13 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) → 𝑧 = 0)
79		0red 11136	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 0 → 0 ∈ ℝ)
80		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = 0 ∧ 𝑥 = 0) → 𝑥 = 0)
81	80	oveq1d 7373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑥 · 1) = (0 · 1))
82	81	eqeq2d 2748	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 = 0 ∧ 𝑥 = 0) → (𝑧 = (𝑥 · 1) ↔ 𝑧 = (0 · 1)))
83	82	anbi1d 632	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 = 0 ∧ 𝑥 = 0) → ((𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i))))
84	83	rexbidv 3162	. . . . . . . . . . . . . 14 ⊢ ((𝑧 = 0 ∧ 𝑥 = 0) → (∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i))))
85		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = 0 ∧ 𝑦 = 0) → 𝑦 = 0)
86	85	oveq1d 7373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑦 · i) = (0 · i))
87	86	eqeq2d 2748	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 = 0 ∧ 𝑦 = 0) → (𝑧 = (𝑦 · i) ↔ 𝑧 = (0 · i)))
88	87	anbi2d 631	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 = 0 ∧ 𝑦 = 0) → ((𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i))))
89	20	mul02i 11324	. . . . . . . . . . . . . . . . . 18 ⊢ (0 · 1) = 0
90	89	eqeq2i 2750	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (0 · 1) ↔ 𝑧 = 0)
91	90	biimpri 228	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 0 → 𝑧 = (0 · 1))
92	28	mul02i 11324	. . . . . . . . . . . . . . . . . 18 ⊢ (0 · i) = 0
93	92	eqeq2i 2750	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (0 · i) ↔ 𝑧 = 0)
94	93	biimpri 228	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 0 → 𝑧 = (0 · i))
95	91, 94	jca 511	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 0 → (𝑧 = (0 · 1) ∧ 𝑧 = (0 · i)))
96	79, 88, 95	rspcedvd 3567	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 0 → ∃𝑦 ∈ ℝ (𝑧 = (0 · 1) ∧ 𝑧 = (𝑦 · i)))
97	79, 84, 96	rspcedvd 3567	. . . . . . . . . . . . 13 ⊢ (𝑧 = 0 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)))
98	78, 97	impbii 209	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ (𝑧 = (𝑥 · 1) ∧ 𝑧 = (𝑦 · i)) ↔ 𝑧 = 0)
99	47, 48, 98	3bitr2i 299	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{i})) ↔ 𝑧 = 0)
100		elin 3906	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{i})) ↔ (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1}) ∧ 𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{i})))
101		velsn 4584	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {0} ↔ 𝑧 = 0)
102	99, 100, 101	3bitr4i 303	. . . . . . . . . 10 ⊢ (𝑧 ∈ (((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{i})) ↔ 𝑧 ∈ {0})
103	102	eqriv 2734	. . . . . . . . 9 ⊢ (((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{i})) = {0}
104	103	a1i 11	. . . . . . . 8 ⊢ (⊤ → (((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1}) ∩ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{i})) = {0})
105	9, 18, 19, 27, 32, 104	lindsun 33790	. . . . . . 7 ⊢ (⊤ → ({1} ∪ {i}) ∈ (LIndS‘((subringAlg ‘ℂ_fld)‘ℝ)))
106	105	mptru 1549	. . . . . 6 ⊢ ({1} ∪ {i}) ∈ (LIndS‘((subringAlg ‘ℂ_fld)‘ℝ))
107	8, 106	eqeltri 2833	. . . . 5 ⊢ {1, i} ∈ (LIndS‘((subringAlg ‘ℂ_fld)‘ℝ))
108		cnfldadd 21348	. . . . . . . . . 10 ⊢ + = (+_g‘ℂ_fld)
109	10, 16	sraaddg 21163	. . . . . . . . . . 11 ⊢ (⊤ → (+_g‘ℂ_fld) = (+_g‘((subringAlg ‘ℂ_fld)‘ℝ)))
110	109	mptru 1549	. . . . . . . . . 10 ⊢ (+_g‘ℂ_fld) = (+_g‘((subringAlg ‘ℂ_fld)‘ℝ))
111	108, 110	eqtri 2760	. . . . . . . . 9 ⊢ + = (+_g‘((subringAlg ‘ℂ_fld)‘ℝ))
112	34	a1i 11	. . . . . . . . 9 ⊢ (⊤ → ((subringAlg ‘ℂ_fld)‘ℝ) ∈ LMod)
113		1cnd 11128	. . . . . . . . 9 ⊢ (⊤ → 1 ∈ ℂ)
114	28	a1i 11	. . . . . . . . 9 ⊢ (⊤ → i ∈ ℂ)
115	24, 111, 38, 4, 42, 9, 112, 113, 114	lspprel 21079	. . . . . . . 8 ⊢ (⊤ → (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i))))
116	115	mptru 1549	. . . . . . 7 ⊢ (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1, i}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)))
117		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ)
118	117	recnd 11162	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℂ)
119		1cnd 11128	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
120	118, 119	mulcld 11154	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 1) ∈ ℂ)
121		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
122	121	recnd 11162	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
123	28	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → i ∈ ℂ)
124	122, 123	mulcld 11154	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · i) ∈ ℂ)
125	120, 124	addcld 11153	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + (𝑦 · i)) ∈ ℂ)
126		eleq1 2825	. . . . . . . . . 10 ⊢ (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → (𝑧 ∈ ℂ ↔ ((𝑥 · 1) + (𝑦 · i)) ∈ ℂ))
127	125, 126	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈ ℂ))
128	127	rexlimivv 3180	. . . . . . . 8 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) → 𝑧 ∈ ℂ)
129		recl 15061	. . . . . . . . 9 ⊢ (𝑧 ∈ ℂ → (ℜ‘𝑧) ∈ ℝ)
130		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → 𝑥 = (ℜ‘𝑧))
131	130	oveq1d 7373	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑥 · 1) = ((ℜ‘𝑧) · 1))
132	131	oveq1d 7373	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → ((𝑥 · 1) + (𝑦 · i)) = (((ℜ‘𝑧) · 1) + (𝑦 · i)))
133	132	eqeq2d 2748	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i))))
134	133	rexbidv 3162	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 = (ℜ‘𝑧)) → (∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ ∃𝑦 ∈ ℝ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i))))
135		imcl 15062	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℂ → (ℑ‘𝑧) ∈ ℝ)
136		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → 𝑦 = (ℑ‘𝑧))
137	136	oveq1d 7373	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑦 · i) = ((ℑ‘𝑧) · i))
138	137	oveq2d 7374	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (((ℜ‘𝑧) · 1) + (𝑦 · i)) = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)))
139	138	eqeq2d 2748	. . . . . . . . . 10 ⊢ ((𝑧 ∈ ℂ ∧ 𝑦 = (ℑ‘𝑧)) → (𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)) ↔ 𝑧 = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i))))
140		replim 15067	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℂ → 𝑧 = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
141	129	recnd 11162	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℂ → (ℜ‘𝑧) ∈ ℂ)
142	141	mulridd 11151	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℂ → ((ℜ‘𝑧) · 1) = (ℜ‘𝑧))
143	135	recnd 11162	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℂ → (ℑ‘𝑧) ∈ ℂ)
144	28	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ℂ → i ∈ ℂ)
145	143, 144	mulcomd 11155	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℂ → ((ℑ‘𝑧) · i) = (i · (ℑ‘𝑧)))
146	142, 145	oveq12d 7376	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ℂ → (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)) = ((ℜ‘𝑧) + (i · (ℑ‘𝑧))))
147	140, 146	eqtr4d 2775	. . . . . . . . . 10 ⊢ (𝑧 ∈ ℂ → 𝑧 = (((ℜ‘𝑧) · 1) + ((ℑ‘𝑧) · i)))
148	135, 139, 147	rspcedvd 3567	. . . . . . . . 9 ⊢ (𝑧 ∈ ℂ → ∃𝑦 ∈ ℝ 𝑧 = (((ℜ‘𝑧) · 1) + (𝑦 · i)))
149	129, 134, 148	rspcedvd 3567	. . . . . . . 8 ⊢ (𝑧 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)))
150	128, 149	impbii 209	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = ((𝑥 · 1) + (𝑦 · i)) ↔ 𝑧 ∈ ℂ)
151	116, 150	bitri 275	. . . . . 6 ⊢ (𝑧 ∈ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1, i}) ↔ 𝑧 ∈ ℂ)
152	151	eqriv 2734	. . . . 5 ⊢ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1, i}) = ℂ
153		eqid 2737	. . . . . 6 ⊢ (LBasis‘((subringAlg ‘ℂ_fld)‘ℝ)) = (LBasis‘((subringAlg ‘ℂ_fld)‘ℝ))
154	24, 153, 9	islbs4 21820	. . . . 5 ⊢ ({1, i} ∈ (LBasis‘((subringAlg ‘ℂ_fld)‘ℝ)) ↔ ({1, i} ∈ (LIndS‘((subringAlg ‘ℂ_fld)‘ℝ)) ∧ ((LSpan‘((subringAlg ‘ℂ_fld)‘ℝ))‘{1, i}) = ℂ))
155	107, 152, 154	mpbir2an 712	. . . 4 ⊢ {1, i} ∈ (LBasis‘((subringAlg ‘ℂ_fld)‘ℝ))
156	153	dimval 33765	. . . 4 ⊢ ((((subringAlg ‘ℂ_fld)‘ℝ) ∈ LVec ∧ {1, i} ∈ (LBasis‘((subringAlg ‘ℂ_fld)‘ℝ))) → (dim‘((subringAlg ‘ℂ_fld)‘ℝ)) = (♯‘{1, i}))
157	7, 155, 156	mp2an 693	. . 3 ⊢ (dim‘((subringAlg ‘ℂ_fld)‘ℝ)) = (♯‘{1, i})
158		1nei 32830	. . . 4 ⊢ 1 ≠ i
159		hashprg 14346	. . . . 5 ⊢ ((1 ∈ ℂ ∧ i ∈ ℂ) → (1 ≠ i ↔ (♯‘{1, i}) = 2))
160	20, 28, 159	mp2an 693	. . . 4 ⊢ (1 ≠ i ↔ (♯‘{1, i}) = 2)
161	158, 160	mpbi 230	. . 3 ⊢ (♯‘{1, i}) = 2
162	157, 161	eqtri 2760	. 2 ⊢ (dim‘((subringAlg ‘ℂ_fld)‘ℝ)) = 2
163	3, 6, 162	3eqtr2i 2766	1 ⊢ (ℂ_fld[:]ℝ_fld) = 2

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1542 ⊤wtru 1543 ∈ wcel 2114 ≠ wne 2933 ∃wrex 3062 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 {csn 4568 {cpr 4570 class class class wbr 5086 ‘cfv 6490 (class class class)co 7358 ℂcc 11025 ℝcr 11026 0cc0 11027 1c1 11028 ici 11029 + caddc 11030 · cmul 11032 − cmin 11366 -cneg 11367 2c2 12225 ♯chash 14281 ℜcre 15048 ℑcim 15049 Basecbs 17168 ↾_s cress 17189 +_gcplusg 17209 ._rcmulr 17210 Scalarcsca 17212 ·_𝑠 cvsca 17213 0_gc0g 17391 LModclmod 20844 LSpanclspn 20955 LBasisclbs 21059 LVecclvec 21087 subringAlg csra 21156 ℂ_fldccnfld 21342 ℝ_fldcrefld 21592 LIndSclinds 21793 dimcldim 33763 /_FldExtcfldext 33803 [:]cextdg 33805

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-reg 9498 ax-inf2 9551 ax-ac2 10374 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104 ax-addf 11106 ax-mulf 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-isom 6499 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-tpos 8167 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-2o 8397 df-oadd 8400 df-er 8634 df-map 8766 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-oi 9416 df-r1 9677 df-rank 9678 df-dju 9814 df-card 9852 df-acn 9855 df-ac 10027 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12164 df-2 12233 df-3 12234 df-4 12235 df-5 12236 df-6 12237 df-7 12238 df-8 12239 df-9 12240 df-n0 12427 df-xnn0 12500 df-z 12514 df-dec 12634 df-uz 12778 df-fz 13451 df-hash 14282 df-cj 15050 df-re 15051 df-im 15052 df-struct 17106 df-sets 17123 df-slot 17141 df-ndx 17153 df-base 17169 df-ress 17190 df-plusg 17222 df-mulr 17223 df-starv 17224 df-sca 17225 df-vsca 17226 df-ip 17227 df-tset 17228 df-ple 17229 df-ocomp 17230 df-ds 17231 df-unif 17232 df-0g 17393 df-mre 17537 df-mrc 17538 df-mri 17539 df-acs 17540 df-proset 18249 df-drs 18250 df-poset 18268 df-ipo 18483 df-mgm 18597 df-sgrp 18676 df-mnd 18692 df-submnd 18741 df-grp 18901 df-minusg 18902 df-sbg 18903 df-subg 19088 df-cntz 19281 df-lsm 19600 df-cmn 19746 df-abl 19747 df-mgp 20111 df-rng 20123 df-ur 20152 df-ring 20205 df-cring 20206 df-oppr 20306 df-dvdsr 20326 df-unit 20327 df-invr 20357 df-dvr 20370 df-subrng 20512 df-subrg 20536 df-drng 20697 df-field 20698 df-lmod 20846 df-lss 20916 df-lsp 20956 df-lbs 21060 df-lvec 21088 df-sra 21158 df-cnfld 21343 df-refld 21593 df-lindf 21794 df-linds 21795 df-dim 33764 df-fldext 33806 df-extdg 33807

This theorem is referenced by: (None)

W3C validator