Metamath Proof Explorer

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 ⊢ R = ringLMod ⁡ ℝ fld
Assertion recvs ⊢ R ∈ ℂVec

Proof

Step Hyp Ref Expression
1 recvs.r ⊢ 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 ↾ 𝑠 ℝ
11 9 10 eqtr3i ⊢ Scalar ⁡ ringLMod ⁡ ℝ fld = ℂ fld ↾ 𝑠 ℝ
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 ↾ 𝑠 ℝ ∧ ℝ ∈ SubRing ⁡ ℂ fld → ringLMod ⁡ ℝ fld ∈ CMod
16 7 11 13 15 mp3an ⊢ ringLMod ⁡ ℝ fld ∈ CMod
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 ∈ CMod ∩ LVec
21 df-cvs ⊢ ℂVec = CMod ∩ LVec
22 20 1 21 3eltr4i ⊢ R ∈ ℂVec