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	|- Q = ( W /s ( W ~QG S ) )
	quslvec.1	|- ( ph -> W e. LVec )
	quslvec.2	|- ( ph -> S e. ( LSubSp ` W ) )
Assertion	quslvec	|- ( ph -> Q e. LVec )

Proof

Step	Hyp	Ref	Expression
1		quslvec.n	|- Q = ( W /s ( W ~QG S ) )
2		quslvec.1	|- ( ph -> W e. LVec )
3		quslvec.2	|- ( ph -> S e. ( LSubSp ` W ) )
4		eqid	|- ( Base ` W ) = ( Base ` W )
5	2	lveclmodd	|- ( ph -> W e. LMod )
6	1 4 5 3	quslmod	|- ( ph -> Q e. LMod )
7	1	a1i	|- ( ph -> Q = ( W /s ( W ~QG S ) ) )
8	4	a1i	|- ( ph -> ( Base ` W ) = ( Base ` W ) )
9		ovexd	|- ( ph -> ( W ~QG S ) e. _V )
10		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
11	7 8 9 2 10	quss	|- ( ph -> ( Scalar ` W ) = ( Scalar ` Q ) )
12	10	lvecdrng	|- ( W e. LVec -> ( Scalar ` W ) e. DivRing )
13	2 12	syl	|- ( ph -> ( Scalar ` W ) e. DivRing )
14	11 13	eqeltrrd	|- ( ph -> ( Scalar ` Q ) e. DivRing )
15		eqid	|- ( Scalar ` Q ) = ( Scalar ` Q )
16	15	islvec	|- ( Q e. LVec <-> ( Q e. LMod /\ ( Scalar ` Q ) e. DivRing ) )
17	6 14 16	sylanbrc	|- ( ph -> Q e. LVec )