recvsOLD

Description: Obsolete version of recvs as of 23-Nov-2024. (Contributed by AV, 22-Oct-2021) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	recvs.r	$⊢ R = ringLMod (ℝ_{fld})$
	Assertion	recvsOLD	$⊢ R \in ℂVec$

Proof

Step	Hyp	Ref	Expression
1		recvs.r	$⊢ R = ringLMod (ℝ_{fld})$
2		refld	$⊢ ℝ_{fld} \in Field$
3		fldidom	$⊢ ℝ_{fld} \in Field \to ℝ_{fld} \in IDomn$
4		isidom	$⊢ ℝ_{fld} \in IDomn \leftrightarrow (ℝ_{fld} \in CRing \land ℝ_{fld} \in Domn)$
5		crngring	$⊢ ℝ_{fld} \in CRing \to ℝ_{fld} \in Ring$
6	5	adantr	$⊢ (ℝ_{fld} \in CRing \land ℝ_{fld} \in Domn) \to ℝ_{fld} \in Ring$
7	4 6	sylbi	$⊢ ℝ_{fld} \in IDomn \to ℝ_{fld} \in Ring$
8	3 7	syl	$⊢ ℝ_{fld} \in Field \to ℝ_{fld} \in Ring$
9	2 8	ax-mp	$⊢ ℝ_{fld} \in Ring$
10		rlmlmod	$⊢ ℝ_{fld} \in Ring \to ringLMod (ℝ_{fld}) \in LMod$
11	9 10	ax-mp	$⊢ ringLMod (ℝ_{fld}) \in LMod$
12		rlmsca	$⊢ ℝ_{fld} \in Field \to ℝ_{fld} = Scalar (ringLMod (ℝ_{fld}))$
13	2 12	ax-mp	$⊢ ℝ_{fld} = Scalar (ringLMod (ℝ_{fld}))$
14		df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$
15	13 14	eqtr3i	$⊢ Scalar (ringLMod (ℝ_{fld})) = ℂ_{fld} ↾_{𝑠} ℝ$
16		resubdrg	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land ℝ_{fld} \in DivRing)$
17	16	simpli	$⊢ ℝ \in SubRing (ℂ_{fld})$
18		eqid	$⊢ Scalar (ringLMod (ℝ_{fld})) = Scalar (ringLMod (ℝ_{fld}))$
19	18	isclmi	$⊢ (ringLMod (ℝ_{fld}) \in LMod \land Scalar (ringLMod (ℝ_{fld})) = ℂ_{fld} ↾_{𝑠} ℝ \land ℝ \in SubRing (ℂ_{fld})) \to ringLMod (ℝ_{fld}) \in CMod$
20	11 15 17 19	mp3an	$⊢ ringLMod (ℝ_{fld}) \in CMod$
21	16	simpri	$⊢ ℝ_{fld} \in DivRing$
22		rlmlvec	$⊢ ℝ_{fld} \in DivRing \to ringLMod (ℝ_{fld}) \in LVec$
23	21 22	ax-mp	$⊢ ringLMod (ℝ_{fld}) \in LVec$
24	20 23	elini	$⊢ ringLMod (ℝ_{fld}) \in (CMod \cap LVec)$
25		df-cvs	$⊢ ℂVec = CMod \cap LVec$
26	24 1 25	3eltr4i	$⊢ R \in ℂVec$

Metamath Proof Explorer

Theorem recvsOLD

Proof