Theorem bj-rveccmod

Description: Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024)

	Ref	Expression
Assertion	bj-rveccmod	⊢ ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod )

Proof

Step	Hyp	Ref	Expression
1		bj-rvecmod	⊢ ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ LMod )
2		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
3	2	a1i	⊢ ( 𝑉 ∈ ℝ-Vec → ℝfld = ( ℂfld ↾s ℝ ) )
4		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
5	4	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂfld )
6	5	a1i	⊢ ( 𝑉 ∈ ℝ-Vec → ℝ ∈ ( SubRing ‘ ℂfld ) )
7		bj-rvecrr	⊢ ( 𝑉 ∈ ℝ-Vec → ( Scalar ‘ 𝑉 ) = ℝfld )
8	7	eqcomd	⊢ ( 𝑉 ∈ ℝ-Vec → ℝfld = ( Scalar ‘ 𝑉 ) )
9		rebase	⊢ ℝ = ( Base ‘ ℝfld )
10	9	a1i	⊢ ( 𝑉 ∈ ℝ-Vec → ℝ = ( Base ‘ ℝfld ) )
11	8 10	bj-isclm	⊢ ( 𝑉 ∈ ℝ-Vec → ( 𝑉 ∈ ℂMod ↔ ( 𝑉 ∈ LMod ∧ ℝfld = ( ℂfld ↾s ℝ ) ∧ ℝ ∈ ( SubRing ‘ ℂfld ) ) ) )
12	1 3 6 11	mpbir3and	⊢ ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂMod )