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)

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 fldidom ⊢ ℝ fld ∈ Field → ℝ fld ∈ IDomn
4 isidom ⊢ ℝ fld ∈ IDomn ↔ ℝ fld ∈ CRing ∧ ℝ fld ∈ Domn
5 crngring ⊢ ℝ fld ∈ CRing → ℝ fld ∈ Ring
6 5 adantr ⊢ ℝ fld ∈ CRing ∧ ℝ fld ∈ Domn → ℝ fld ∈ Ring
7 4 6 sylbi ⊢ ℝ fld ∈ IDomn → ℝ fld ∈ Ring
8 3 7 syl ⊢ ℝ fld ∈ Field → ℝ fld ∈ Ring
9 2 8 ax-mp ⊢ ℝ fld ∈ Ring
10 rlmlmod ⊢ ℝ fld ∈ Ring → ringLMod ⁡ ℝ fld ∈ LMod
11 9 10 ax-mp ⊢ ringLMod ⁡ ℝ fld ∈ LMod
12 rlmsca ⊢ ℝ fld ∈ Field → ℝ fld = Scalar ⁡ ringLMod ⁡ ℝ fld
13 2 12 ax-mp ⊢ ℝ fld = Scalar ⁡ ringLMod ⁡ ℝ fld
14 df-refld ⊢ ℝ fld = ℂ fld ↾ 𝑠 ℝ
15 13 14 eqtr3i ⊢ Scalar ⁡ ringLMod ⁡ ℝ fld = ℂ fld ↾ 𝑠 ℝ
16 resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing
17 16 simpli ⊢ ℝ ∈ SubRing ⁡ ℂ fld
18 eqid ⊢ Scalar ⁡ ringLMod ⁡ ℝ fld = Scalar ⁡ ringLMod ⁡ ℝ fld
19 18 isclmi ⊢ ringLMod ⁡ ℝ fld ∈ LMod ∧ Scalar ⁡ ringLMod ⁡ ℝ fld = ℂ fld ↾ 𝑠 ℝ ∧ ℝ ∈ SubRing ⁡ ℂ fld → ringLMod ⁡ ℝ fld ∈ CMod
20 11 15 17 19 mp3an ⊢ ringLMod ⁡ ℝ fld ∈ CMod
21 16 simpri ⊢ ℝ fld ∈ DivRing
22 rlmlvec ⊢ ℝ fld ∈ DivRing → ringLMod ⁡ ℝ fld ∈ LVec
23 21 22 ax-mp ⊢ ringLMod ⁡ ℝ fld ∈ LVec
24 20 23 elini ⊢ ringLMod ⁡ ℝ fld ∈ CMod ∩ LVec
25 df-cvs ⊢ ℂVec = CMod ∩ LVec
26 24 1 25 3eltr4i ⊢ R ∈ ℂVec