This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qcvs

Description: The field of rational 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 qcvs.q ⊢ 𝑄 = ( ringLMod ‘ ( ℂfld ↾s ℚ ) )
Assertion qcvs 𝑄 ∈ ℂVec

Proof

Step Hyp Ref Expression
1 qcvs.q ⊢ 𝑄 = ( ringLMod ‘ ( ℂfld ↾s ℚ ) )
2 qsubdrg ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )
3 drngring ⊢ ( ( ℂfld ↾s ℚ ) ∈ DivRing → ( ℂfld ↾s ℚ ) ∈ Ring )
4 3 adantl ⊢ ( ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing ) → ( ℂfld ↾s ℚ ) ∈ Ring )
5 2 4 ax-mp ⊢ ( ℂfld ↾s ℚ ) ∈ Ring
6 rlmlmod ⊢ ( ( ℂfld ↾s ℚ ) ∈ Ring → ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ∈ LMod )
7 5 6 ax-mp ⊢ ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ∈ LMod
8 2 simpri ⊢ ( ℂfld ↾s ℚ ) ∈ DivRing
9 rlmsca ⊢ ( ( ℂfld ↾s ℚ ) ∈ DivRing → ( ℂfld ↾s ℚ ) = ( Scalar ‘ ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ) )
10 9 eqcomd ⊢ ( ( ℂfld ↾s ℚ ) ∈ DivRing → ( Scalar ‘ ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ) = ( ℂfld ↾s ℚ ) )
11 8 10 ax-mp ⊢ ( Scalar ‘ ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ) = ( ℂfld ↾s ℚ )
12 2 simpli ⊢ ℚ ∈ ( SubRing ‘ ℂfld )
13 eqid ⊢ ( Scalar ‘ ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ) = ( Scalar ‘ ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) )
14 13 isclmi ⊢ ( ( ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ∈ LMod ∧ ( Scalar ‘ ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ) = ( ℂfld ↾s ℚ ) ∧ ℚ ∈ ( SubRing ‘ ℂfld ) ) → ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ∈ ℂMod )
15 7 11 12 14 mp3an ⊢ ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ∈ ℂMod
16 rlmlvec ⊢ ( ( ℂfld ↾s ℚ ) ∈ DivRing → ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ∈ LVec )
17 8 16 ax-mp ⊢ ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ∈ LVec
18 15 17 elini ⊢ ( ringLMod ‘ ( ℂfld ↾s ℚ ) ) ∈ ( ℂMod ∩ LVec )
19 df-cvs ⊢ ℂVec = ( ℂMod ∩ LVec )
20 18 1 19 3eltr4i ⊢ 𝑄 ∈ ℂVec