Theorem recvs

Description: The field of the real numbers as left module over itself is a subcomplex vector space. The vector operation is + , and the scalar product is x. . (Contributed by AV, 22-Oct-2021)

	Ref	Expression
Hypothesis	recvs.r	⊢ 𝑅 = ( ringLMod ‘ ℝfld )
Assertion	recvs	⊢ 𝑅 ∈ ℂVec

Proof

Step	Hyp	Ref	Expression
1		recvs.r	⊢ 𝑅 = ( ringLMod ‘ ℝfld )
2		refld	⊢ ℝfld ∈ Field
3		fldidom	⊢ ( ℝfld ∈ Field → ℝfld ∈ IDomn )
4		isidom	⊢ ( ℝfld ∈ IDomn ↔ ( ℝfld ∈ CRing ∧ ℝfld ∈ Domn ) )
5		crngring	⊢ ( ℝfld ∈ CRing → ℝfld ∈ Ring )
6	5	adantr	⊢ ( ( ℝfld ∈ CRing ∧ ℝfld ∈ Domn ) → ℝfld ∈ Ring )
7	4 6	sylbi	⊢ ( ℝfld ∈ IDomn → ℝfld ∈ Ring )
8	3 7	syl	⊢ ( ℝfld ∈ Field → ℝfld ∈ Ring )
9	2 8	ax-mp	⊢ ℝfld ∈ Ring
10		rlmlmod	⊢ ( ℝfld ∈ Ring → ( ringLMod ‘ ℝfld ) ∈ LMod )
11	9 10	ax-mp	⊢ ( ringLMod ‘ ℝfld ) ∈ LMod
12		rlmsca	⊢ ( ℝfld ∈ Field → ℝfld = ( Scalar ‘ ( ringLMod ‘ ℝfld ) ) )
13	2 12	ax-mp	⊢ ℝfld = ( Scalar ‘ ( ringLMod ‘ ℝfld ) )
14		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
15	13 14	eqtr3i	⊢ ( Scalar ‘ ( ringLMod ‘ ℝfld ) ) = ( ℂfld ↾s ℝ )
16		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
17	16	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂfld )
18		eqid	⊢ ( Scalar ‘ ( ringLMod ‘ ℝfld ) ) = ( Scalar ‘ ( ringLMod ‘ ℝfld ) )
19	18	isclmi	⊢ ( ( ( ringLMod ‘ ℝfld ) ∈ LMod ∧ ( Scalar ‘ ( ringLMod ‘ ℝfld ) ) = ( ℂfld ↾s ℝ ) ∧ ℝ ∈ ( SubRing ‘ ℂfld ) ) → ( ringLMod ‘ ℝfld ) ∈ ℂMod )
20	11 15 17 19	mp3an	⊢ ( ringLMod ‘ ℝfld ) ∈ ℂMod
21	16	simpri	⊢ ℝfld ∈ DivRing
22		rlmlvec	⊢ ( ℝfld ∈ DivRing → ( ringLMod ‘ ℝfld ) ∈ LVec )
23	21 22	ax-mp	⊢ ( ringLMod ‘ ℝfld ) ∈ LVec
24	20 23	elini	⊢ ( ringLMod ‘ ℝfld ) ∈ ( ℂMod ∩ LVec )
25		df-cvs	⊢ ℂVec = ( ℂMod ∩ LVec )
26	24 1 25	3eltr4i	⊢ 𝑅 ∈ ℂVec