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