Metamath Proof Explorer

Theorem bj-rveccmod

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

Ref Expression
Assertion bj-rveccmod ⊢ V ∈ ℝVec → V ∈ CMod

Proof

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