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

Metamath Proof Explorer

Theorem lsssssubg

Description: All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016)

		Ref	Expression
	Hypothesis	lsssubg.s	$⊢ S = LSubSp (W)$
	Assertion	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$

Step	Hyp	Ref	Expression
1		lsssubg.s	$⊢ S = LSubSp (W)$
2	1	lsssubg	$⊢ (W \in LMod \land x \in S) \to x \in SubGrp (W)$
3	2	ex	$⊢ W \in LMod \to (x \in S \to x \in SubGrp (W))$
4	3	ssrdv	$⊢ W \in LMod \to S \subseteq SubGrp (W)$