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

Metamath Proof Explorer

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 )