Metamath Proof Explorer

Theorem lsssubg

Description: All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014)

Ref Expression
Hypothesis lsssubg.s 
|- S = ( LSubSp ` W )
Assertion lsssubg 
|- ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) )

Proof

Step Hyp Ref Expression
1 lsssubg.s 
 |-  S = ( LSubSp ` W )
2 eqid 
 |-  ( Base ` W ) = ( Base ` W )
3 2 1 lssss 
 |-  ( U e. S -> U C_ ( Base ` W ) )
4 3 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> U C_ ( Base ` W ) )
5 1 lssn0 
 |-  ( U e. S -> U =/= (/) )
6 5 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> U =/= (/) )
7 eqid 
 |-  ( +g ` W ) = ( +g ` W )
8 7 1 lssvacl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. U /\ y e. U ) ) -> ( x ( +g ` W ) y ) e. U )
9 8 anassrs 
 |-  ( ( ( ( W e. LMod /\ U e. S ) /\ x e. U ) /\ y e. U ) -> ( x ( +g ` W ) y ) e. U )
10 9 ralrimiva 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ x e. U ) -> A. y e. U ( x ( +g ` W ) y ) e. U )
11 eqid 
 |-  ( invg ` W ) = ( invg ` W )
12 1 11 lssvnegcl 
 |-  ( ( W e. LMod /\ U e. S /\ x e. U ) -> ( ( invg ` W ) ` x ) e. U )
13 12 3expa 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ x e. U ) -> ( ( invg ` W ) ` x ) e. U )
14 10 13 jca 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ x e. U ) -> ( A. y e. U ( x ( +g ` W ) y ) e. U /\ ( ( invg ` W ) ` x ) e. U ) )
15 14 ralrimiva 
 |-  ( ( W e. LMod /\ U e. S ) -> A. x e. U ( A. y e. U ( x ( +g ` W ) y ) e. U /\ ( ( invg ` W ) ` x ) e. U ) )
16 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
17 16 adantr 
 |-  ( ( W e. LMod /\ U e. S ) -> W e. Grp )
18 2 7 11 issubg2 
 |-  ( W e. Grp -> ( U e. ( SubGrp ` W ) <-> ( U C_ ( Base ` W ) /\ U =/= (/) /\ A. x e. U ( A. y e. U ( x ( +g ` W ) y ) e. U /\ ( ( invg ` W ) ` x ) e. U ) ) ) )
19 17 18 syl 
 |-  ( ( W e. LMod /\ U e. S ) -> ( U e. ( SubGrp ` W ) <-> ( U C_ ( Base ` W ) /\ U =/= (/) /\ A. x e. U ( A. y e. U ( x ( +g ` W ) y ) e. U /\ ( ( invg ` W ) ` x ) e. U ) ) ) )
20 4 6 15 19 mpbir3and 
 |-  ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) )