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 ⊢ 𝑄 = ( 𝑊 /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 )