Metamath Proof Explorer

Theorem islss4

Description: A linear subspace is a subgroup which respects scalar multiplication. (Contributed by Stefan O'Rear, 11-Dec-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses islss4.f 
|- F = ( Scalar ` W )
islss4.b 
|- B = ( Base ` F )
islss4.v 
|- V = ( Base ` W )
islss4.t 
|- .x. = ( .s ` W )
islss4.s 
|- S = ( LSubSp ` W )
Assertion islss4 
|- ( W e. LMod -> ( U e. S <-> ( U e. ( SubGrp ` W ) /\ A. a e. B A. b e. U ( a .x. b ) e. U ) ) )

Proof

Step Hyp Ref Expression
1 islss4.f 
 |-  F = ( Scalar ` W )
2 islss4.b 
 |-  B = ( Base ` F )
3 islss4.v 
 |-  V = ( Base ` W )
4 islss4.t 
 |-  .x. = ( .s ` W )
5 islss4.s 
 |-  S = ( LSubSp ` W )
6 5 lsssubg 
 |-  ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) )
7 1 4 2 5 lssvscl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( a e. B /\ b e. U ) ) -> ( a .x. b ) e. U )
8 7 ralrimivva 
 |-  ( ( W e. LMod /\ U e. S ) -> A. a e. B A. b e. U ( a .x. b ) e. U )
9 6 8 jca 
 |-  ( ( W e. LMod /\ U e. S ) -> ( U e. ( SubGrp ` W ) /\ A. a e. B A. b e. U ( a .x. b ) e. U ) )
10 3 subgss 
 |-  ( U e. ( SubGrp ` W ) -> U C_ V )
11 10 ad2antrl 
 |-  ( ( W e. LMod /\ ( U e. ( SubGrp ` W ) /\ A. a e. B A. b e. U ( a .x. b ) e. U ) ) -> U C_ V )
12 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
13 12 subg0cl 
 |-  ( U e. ( SubGrp ` W ) -> ( 0g ` W ) e. U )
14 13 ne0d 
 |-  ( U e. ( SubGrp ` W ) -> U =/= (/) )
15 14 ad2antrl 
 |-  ( ( W e. LMod /\ ( U e. ( SubGrp ` W ) /\ A. a e. B A. b e. U ( a .x. b ) e. U ) ) -> U =/= (/) )
16 eqid 
 |-  ( +g ` W ) = ( +g ` W )
17 16 subgcl 
 |-  ( ( U e. ( SubGrp ` W ) /\ ( a .x. b ) e. U /\ c e. U ) -> ( ( a .x. b ) ( +g ` W ) c ) e. U )
18 17 3exp 
 |-  ( U e. ( SubGrp ` W ) -> ( ( a .x. b ) e. U -> ( c e. U -> ( ( a .x. b ) ( +g ` W ) c ) e. U ) ) )
19 18 adantl 
 |-  ( ( W e. LMod /\ U e. ( SubGrp ` W ) ) -> ( ( a .x. b ) e. U -> ( c e. U -> ( ( a .x. b ) ( +g ` W ) c ) e. U ) ) )
20 19 ralrimdv 
 |-  ( ( W e. LMod /\ U e. ( SubGrp ` W ) ) -> ( ( a .x. b ) e. U -> A. c e. U ( ( a .x. b ) ( +g ` W ) c ) e. U ) )
21 20 ralimdv 
 |-  ( ( W e. LMod /\ U e. ( SubGrp ` W ) ) -> ( A. b e. U ( a .x. b ) e. U -> A. b e. U A. c e. U ( ( a .x. b ) ( +g ` W ) c ) e. U ) )
22 21 ralimdv 
 |-  ( ( W e. LMod /\ U e. ( SubGrp ` W ) ) -> ( A. a e. B A. b e. U ( a .x. b ) e. U -> A. a e. B A. b e. U A. c e. U ( ( a .x. b ) ( +g ` W ) c ) e. U ) )
23 22 impr 
 |-  ( ( W e. LMod /\ ( U e. ( SubGrp ` W ) /\ A. a e. B A. b e. U ( a .x. b ) e. U ) ) -> A. a e. B A. b e. U A. c e. U ( ( a .x. b ) ( +g ` W ) c ) e. U )
24 1 2 3 16 4 5 islss 
 |-  ( U e. S <-> ( U C_ V /\ U =/= (/) /\ A. a e. B A. b e. U A. c e. U ( ( a .x. b ) ( +g ` W ) c ) e. U ) )
25 11 15 23 24 syl3anbrc 
 |-  ( ( W e. LMod /\ ( U e. ( SubGrp ` W ) /\ A. a e. B A. b e. U ( a .x. b ) e. U ) ) -> U e. S )
26 9 25 impbida 
 |-  ( W e. LMod -> ( U e. S <-> ( U e. ( SubGrp ` W ) /\ A. a e. B A. b e. U ( a .x. b ) e. U ) ) )