ccfldsrarelvec

Description: The subring algebra of the complex numbers over the real numbers is a left vector space. (Contributed by Thierry Arnoux, 20-Aug-2023)

		Ref	Expression
	Assertion	ccfldsrarelvec	$⊢ subringAlg (ℂ_{fld}) (ℝ) \in LVec$

Proof

Step	Hyp	Ref	Expression
1		cnring	$⊢ ℂ_{fld} \in Ring$
2		ax-resscn	$⊢ ℝ \subseteq ℂ$
3		eqidd	$⊢ ⊤ \to subringAlg (ℂ_{fld}) (ℝ) = subringAlg (ℂ_{fld}) (ℝ)$
4	3	mptru	$⊢ subringAlg (ℂ_{fld}) (ℝ) = subringAlg (ℂ_{fld}) (ℝ)$
5		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
6	4 5	sraring	$⊢ (ℂ_{fld} \in Ring \land ℝ \subseteq ℂ) \to subringAlg (ℂ_{fld}) (ℝ) \in Ring$
7	1 2 6	mp2an	$⊢ subringAlg (ℂ_{fld}) (ℝ) \in Ring$
8		ringgrp	$⊢ subringAlg (ℂ_{fld}) (ℝ) \in Ring \to subringAlg (ℂ_{fld}) (ℝ) \in Grp$
9	7 8	ax-mp	$⊢ subringAlg (ℂ_{fld}) (ℝ) \in Grp$
10		refld	$⊢ ℝ_{fld} \in Field$
11		isfld	$⊢ ℝ_{fld} \in Field \leftrightarrow (ℝ_{fld} \in DivRing \land ℝ_{fld} \in CRing)$
12	10 11	mpbi	$⊢ (ℝ_{fld} \in DivRing \land ℝ_{fld} \in CRing)$
13	12	simpli	$⊢ ℝ_{fld} \in DivRing$
14		drngring	$⊢ ℝ_{fld} \in DivRing \to ℝ_{fld} \in Ring$
15	13 14	ax-mp	$⊢ ℝ_{fld} \in Ring$
16		simpr1	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to b \in ℝ$
17	16	recnd	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to b \in ℂ$
18		simpr3	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to y \in ℂ$
19	17 18	mulcld	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to b y \in ℂ$
20		simpr2	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to x \in ℂ$
21	17 18 20	adddid	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to b (y + x) = b y + b x$
22		simpl	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to a \in ℝ$
23	22	recnd	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to a \in ℂ$
24	23 17 18	adddird	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to (a + b) y = a y + b y$
25	19 21 24	3jca	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to (b y \in ℂ \land b (y + x) = b y + b x \land (a + b) y = a y + b y)$
26	23 17 18	mulassd	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to a b y = a b y$
27	18	mulid2d	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to 1 y = y$
28	25 26 27	jca32	$⊢ (a \in ℝ \land (b \in ℝ \land x \in ℂ \land y \in ℂ)) \to ((b y \in ℂ \land b (y + x) = b y + b x \land (a + b) y = a y + b y) \land (a b y = a b y \land 1 y = y))$
29	28	ralrimivvva	$⊢ a \in ℝ \to \forall b \in ℝ \forall x \in ℂ \forall y \in ℂ ((b y \in ℂ \land b (y + x) = b y + b x \land (a + b) y = a y + b y) \land (a b y = a b y \land 1 y = y))$
30	29	rgen	$⊢ \forall a \in ℝ \forall b \in ℝ \forall x \in ℂ \forall y \in ℂ ((b y \in ℂ \land b (y + x) = b y + b x \land (a + b) y = a y + b y) \land (a b y = a b y \land 1 y = y))$
31	2 5	sseqtri	$⊢ ℝ \subseteq {Base}_{ℂ_{fld}}$
32	31	a1i	$⊢ ⊤ \to ℝ \subseteq {Base}_{ℂ_{fld}}$
33	3 32	srabase	$⊢ ⊤ \to {Base}_{ℂ_{fld}} = {Base}_{subringAlg (ℂ_{fld}) (ℝ)}$
34	33	mptru	$⊢ {Base}_{ℂ_{fld}} = {Base}_{subringAlg (ℂ_{fld}) (ℝ)}$
35	5 34	eqtri	$⊢ ℂ = {Base}_{subringAlg (ℂ_{fld}) (ℝ)}$
36		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
37	3 32	sraaddg	$⊢ ⊤ \to +_{ℂ_{fld}} = +_{subringAlg (ℂ_{fld}) (ℝ)}$
38	37	mptru	$⊢ +_{ℂ_{fld}} = +_{subringAlg (ℂ_{fld}) (ℝ)}$
39	36 38	eqtri	$⊢ + = +_{subringAlg (ℂ_{fld}) (ℝ)}$
40		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
41	3 32	sravsca	$⊢ ⊤ \to \cdot_{ℂ_{fld}} = \cdot_{subringAlg (ℂ_{fld}) (ℝ)}$
42	41	mptru	$⊢ \cdot_{ℂ_{fld}} = \cdot_{subringAlg (ℂ_{fld}) (ℝ)}$
43	40 42	eqtri	$⊢ \times = \cdot_{subringAlg (ℂ_{fld}) (ℝ)}$
44		df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$
45	3 32	srasca	$⊢ ⊤ \to ℂ_{fld} ↾_{𝑠} ℝ = Scalar (subringAlg (ℂ_{fld}) (ℝ))$
46	45	mptru	$⊢ ℂ_{fld} ↾_{𝑠} ℝ = Scalar (subringAlg (ℂ_{fld}) (ℝ))$
47	44 46	eqtri	$⊢ ℝ_{fld} = Scalar (subringAlg (ℂ_{fld}) (ℝ))$
48		rebase	$⊢ ℝ = {Base}_{ℝ_{fld}}$
49		replusg	$⊢ + = +_{ℝ_{fld}}$
50		remulr	$⊢ \times = \cdot_{ℝ_{fld}}$
51		re1r	$⊢ 1 = 1_{ℝ_{fld}}$
52	35 39 43 47 48 49 50 51	islmod	$⊢ subringAlg (ℂ_{fld}) (ℝ) \in LMod \leftrightarrow (subringAlg (ℂ_{fld}) (ℝ) \in Grp \land ℝ_{fld} \in Ring \land \forall a \in ℝ \forall b \in ℝ \forall x \in ℂ \forall y \in ℂ ((b y \in ℂ \land b (y + x) = b y + b x \land (a + b) y = a y + b y) \land (a b y = a b y \land 1 y = y)))$
53	9 15 30 52	mpbir3an	$⊢ subringAlg (ℂ_{fld}) (ℝ) \in LMod$
54	47	islvec	$⊢ subringAlg (ℂ_{fld}) (ℝ) \in LVec \leftrightarrow (subringAlg (ℂ_{fld}) (ℝ) \in LMod \land ℝ_{fld} \in DivRing)$
55	53 13 54	mpbir2an	$⊢ subringAlg (ℂ_{fld}) (ℝ) \in LVec$

Metamath Proof Explorer

Theorem ccfldsrarelvec

Proof