| 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 ) ) |