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 e. LMod -> S C_ ( SubGrp ` W ) )

Proof

Step Hyp Ref Expression
1 lsssubg.s 
 |-  S = ( LSubSp ` W )
2 1 lsssubg 
 |-  ( ( W e. LMod /\ x e. S ) -> x e. ( SubGrp ` W ) )
3 2 ex 
 |-  ( W e. LMod -> ( x e. S -> x e. ( SubGrp ` W ) ) )
4 3 ssrdv 
 |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )