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

Metamath Proof Explorer

Theorem recvs

Proof