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 /_{𝑠} (W ~_{QG} S)$
		quslvec.1	$⊢ φ \to W \in LVec$
		quslvec.2	$⊢ φ \to S \in LSubSp (W)$
	Assertion	quslvec	$⊢ φ \to Q \in LVec$

Proof

Step	Hyp	Ref	Expression
1		quslvec.n	$⊢ Q = W /_{𝑠} (W ~_{QG} S)$
2		quslvec.1	$⊢ φ \to W \in LVec$
3		quslvec.2	$⊢ φ \to S \in LSubSp (W)$
4		eqid	$⊢ {Base}_{W} = {Base}_{W}$
5	2	lveclmodd	$⊢ φ \to W \in LMod$
6	1 4 5 3	quslmod	$⊢ φ \to Q \in LMod$
7	1	a1i	$⊢ φ \to Q = W /_{𝑠} (W ~_{QG} S)$
8	4	a1i	$⊢ φ \to {Base}_{W} = {Base}_{W}$
9		ovexd	$⊢ φ \to W ~_{QG} S \in V$
10		eqid	$⊢ Scalar (W) = Scalar (W)$
11	7 8 9 2 10	quss	$⊢ φ \to Scalar (W) = Scalar (Q)$
12	10	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
13	2 12	syl	$⊢ φ \to Scalar (W) \in DivRing$
14	11 13	eqeltrrd	$⊢ φ \to Scalar (Q) \in DivRing$
15		eqid	$⊢ Scalar (Q) = Scalar (Q)$
16	15	islvec	$⊢ Q \in LVec \leftrightarrow (Q \in LMod \land Scalar (Q) \in DivRing)$
17	6 14 16	sylanbrc	$⊢ φ \to Q \in LVec$