Theorem quslvec

Description: If S is a vector subspace in W , then Q = W / S is a vector space, called the quotient space of W by S . (Contributed by Thierry Arnoux, 18-May-2023)

	Ref	Expression
Hypotheses	quslvec.n	⊢ 𝑄 = ( 𝑊 /s ( 𝑊 ~QG 𝑆 ) )
	quslvec.1	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	quslvec.2	⊢ ( 𝜑 → 𝑆 ∈ ( LSubSp ‘ 𝑊 ) )
Assertion	quslvec	⊢ ( 𝜑 → 𝑄 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		quslvec.n	⊢ 𝑄 = ( 𝑊 /s ( 𝑊 ~QG 𝑆 ) )
2		quslvec.1	⊢ ( 𝜑 → 𝑊 ∈ LVec )
3		quslvec.2	⊢ ( 𝜑 → 𝑆 ∈ ( LSubSp ‘ 𝑊 ) )
4		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5	2	lveclmodd	⊢ ( 𝜑 → 𝑊 ∈ LMod )
6	1 4 5 3	quslmod	⊢ ( 𝜑 → 𝑄 ∈ LMod )
7	1	a1i	⊢ ( 𝜑 → 𝑄 = ( 𝑊 /s ( 𝑊 ~QG 𝑆 ) ) )
8	4	a1i	⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
9		ovexd	⊢ ( 𝜑 → ( 𝑊 ~QG 𝑆 ) ∈ V )
10		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
11	7 8 9 2 10	quss	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑄 ) )
12	10	lvecdrng	⊢ ( 𝑊 ∈ LVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
13	2 12	syl	⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) ∈ DivRing )
14	11 13	eqeltrrd	⊢ ( 𝜑 → ( Scalar ‘ 𝑄 ) ∈ DivRing )
15		eqid	⊢ ( Scalar ‘ 𝑄 ) = ( Scalar ‘ 𝑄 )
16	15	islvec	⊢ ( 𝑄 ∈ LVec ↔ ( 𝑄 ∈ LMod ∧ ( Scalar ‘ 𝑄 ) ∈ DivRing ) )
17	6 14 16	sylanbrc	⊢ ( 𝜑 → 𝑄 ∈ LVec )