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) (Proof shortened by SN, 23-Nov-2024)

	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		isfld	⊢ ( ℝfld ∈ Field ↔ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing ) )
4	3	simprbi	⊢ ( ℝfld ∈ Field → ℝfld ∈ CRing )
5	4	crngringd	⊢ ( ℝfld ∈ Field → ℝfld ∈ Ring )
6		rlmlmod	⊢ ( ℝfld ∈ Ring → ( ringLMod ‘ ℝfld ) ∈ LMod )
7	2 5 6	mp2b	⊢ ( ringLMod ‘ ℝfld ) ∈ LMod
8		rlmsca	⊢ ( ℝfld ∈ Field → ℝfld = ( Scalar ‘ ( ringLMod ‘ ℝfld ) ) )
9	2 8	ax-mp	⊢ ℝfld = ( Scalar ‘ ( ringLMod ‘ ℝfld ) )
10		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
11	9 10	eqtr3i	⊢ ( Scalar ‘ ( ringLMod ‘ ℝfld ) ) = ( ℂfld ↾s ℝ )
12		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
13	12	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂfld )
14		eqid	⊢ ( Scalar ‘ ( ringLMod ‘ ℝfld ) ) = ( Scalar ‘ ( ringLMod ‘ ℝfld ) )
15	14	isclmi	⊢ ( ( ( ringLMod ‘ ℝfld ) ∈ LMod ∧ ( Scalar ‘ ( ringLMod ‘ ℝfld ) ) = ( ℂfld ↾s ℝ ) ∧ ℝ ∈ ( SubRing ‘ ℂfld ) ) → ( ringLMod ‘ ℝfld ) ∈ ℂMod )
16	7 11 13 15	mp3an	⊢ ( ringLMod ‘ ℝfld ) ∈ ℂMod
17	12	simpri	⊢ ℝfld ∈ DivRing
18		rlmlvec	⊢ ( ℝfld ∈ DivRing → ( ringLMod ‘ ℝfld ) ∈ LVec )
19	17 18	ax-mp	⊢ ( ringLMod ‘ ℝfld ) ∈ LVec
20	16 19	elini	⊢ ( ringLMod ‘ ℝfld ) ∈ ( ℂMod ∩ LVec )
21		df-cvs	⊢ ℂVec = ( ℂMod ∩ LVec )
22	20 1 21	3eltr4i	⊢ 𝑅 ∈ ℂVec