Metamath Proof Explorer

Theorem islss3

Description: A linear subspace of a module is a subset which is a module in its own right. (Contributed by Stefan O'Rear, 6-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses islss3.x 
|- X = ( W |`s U )
islss3.v 
|- V = ( Base ` W )
islss3.s 
|- S = ( LSubSp ` W )
Assertion islss3 
|- ( W e. LMod -> ( U e. S <-> ( U C_ V /\ X e. LMod ) ) )

Proof

Step Hyp Ref Expression
1 islss3.x 
 |-  X = ( W |`s U )
2 islss3.v 
 |-  V = ( Base ` W )
3 islss3.s 
 |-  S = ( LSubSp ` W )
4 2 3 lssss 
 |-  ( U e. S -> U C_ V )
5 4 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> U C_ V )
6 1 2 ressbas2 
 |-  ( U C_ V -> U = ( Base ` X ) )
7 6 adantl 
 |-  ( ( W e. LMod /\ U C_ V ) -> U = ( Base ` X ) )
8 4 7 sylan2 
 |-  ( ( W e. LMod /\ U e. S ) -> U = ( Base ` X ) )
9 eqid 
 |-  ( +g ` W ) = ( +g ` W )
10 1 9 ressplusg 
 |-  ( U e. S -> ( +g ` W ) = ( +g ` X ) )
11 10 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> ( +g ` W ) = ( +g ` X ) )
12 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
13 1 12 resssca 
 |-  ( U e. S -> ( Scalar ` W ) = ( Scalar ` X ) )
14 13 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> ( Scalar ` W ) = ( Scalar ` X ) )
15 eqid 
 |-  ( .s ` W ) = ( .s ` W )
16 1 15 ressvsca 
 |-  ( U e. S -> ( .s ` W ) = ( .s ` X ) )
17 16 adantl 
 |-  ( ( W e. LMod /\ U e. S ) -> ( .s ` W ) = ( .s ` X ) )
18 eqidd 
 |-  ( ( W e. LMod /\ U e. S ) -> ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) )
19 eqidd 
 |-  ( ( W e. LMod /\ U e. S ) -> ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) ) )
20 eqidd 
 |-  ( ( W e. LMod /\ U e. S ) -> ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) ) )
21 eqidd 
 |-  ( ( W e. LMod /\ U e. S ) -> ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) ) )
22 12 lmodring 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Ring )
23 22 adantr 
 |-  ( ( W e. LMod /\ U e. S ) -> ( Scalar ` W ) e. Ring )
24 3 lsssubg 
 |-  ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) )
25 1 subggrp 
 |-  ( U e. ( SubGrp ` W ) -> X e. Grp )
26 24 25 syl 
 |-  ( ( W e. LMod /\ U e. S ) -> X e. Grp )
27 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
28 12 15 27 3 lssvscl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. U ) ) -> ( x ( .s ` W ) a ) e. U )
29 28 3impb 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ x e. ( Base ` ( Scalar ` W ) ) /\ a e. U ) -> ( x ( .s ` W ) a ) e. U )
30 simpll 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. U /\ b e. U ) ) -> W e. LMod )
31 simpr1 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. U /\ b e. U ) ) -> x e. ( Base ` ( Scalar ` W ) ) )
32 4 ad2antlr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. U /\ b e. U ) ) -> U C_ V )
33 simpr2 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. U /\ b e. U ) ) -> a e. U )
34 32 33 sseldd 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. U /\ b e. U ) ) -> a e. V )
35 simpr3 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. U /\ b e. U ) ) -> b e. U )
36 32 35 sseldd 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. U /\ b e. U ) ) -> b e. V )
37 2 9 12 15 27 lmodvsdi 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. V /\ b e. V ) ) -> ( x ( .s ` W ) ( a ( +g ` W ) b ) ) = ( ( x ( .s ` W ) a ) ( +g ` W ) ( x ( .s ` W ) b ) ) )
38 30 31 34 36 37 syl13anc 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. U /\ b e. U ) ) -> ( x ( .s ` W ) ( a ( +g ` W ) b ) ) = ( ( x ( .s ` W ) a ) ( +g ` W ) ( x ( .s ` W ) b ) ) )
39 simpll 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. ( Base ` ( Scalar ` W ) ) /\ b e. U ) ) -> W e. LMod )
40 simpr1 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. ( Base ` ( Scalar ` W ) ) /\ b e. U ) ) -> x e. ( Base ` ( Scalar ` W ) ) )
41 simpr2 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. ( Base ` ( Scalar ` W ) ) /\ b e. U ) ) -> a e. ( Base ` ( Scalar ` W ) ) )
42 4 ad2antlr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. ( Base ` ( Scalar ` W ) ) /\ b e. U ) ) -> U C_ V )
43 simpr3 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. ( Base ` ( Scalar ` W ) ) /\ b e. U ) ) -> b e. U )
44 42 43 sseldd 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. ( Base ` ( Scalar ` W ) ) /\ b e. U ) ) -> b e. V )
45 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
46 2 9 12 15 27 45 lmodvsdir 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. ( Base ` ( Scalar ` W ) ) /\ b e. V ) ) -> ( ( x ( +g ` ( Scalar ` W ) ) a ) ( .s ` W ) b ) = ( ( x ( .s ` W ) b ) ( +g ` W ) ( a ( .s ` W ) b ) ) )
47 39 40 41 44 46 syl13anc 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. ( Base ` ( Scalar ` W ) ) /\ b e. U ) ) -> ( ( x ( +g ` ( Scalar ` W ) ) a ) ( .s ` W ) b ) = ( ( x ( .s ` W ) b ) ( +g ` W ) ( a ( .s ` W ) b ) ) )
48 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
49 2 12 15 27 48 lmodvsass 
 |-  ( ( W e. LMod /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. ( Base ` ( Scalar ` W ) ) /\ b e. V ) ) -> ( ( x ( .r ` ( Scalar ` W ) ) a ) ( .s ` W ) b ) = ( x ( .s ` W ) ( a ( .s ` W ) b ) ) )
50 39 40 41 44 49 syl13anc 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( x e. ( Base ` ( Scalar ` W ) ) /\ a e. ( Base ` ( Scalar ` W ) ) /\ b e. U ) ) -> ( ( x ( .r ` ( Scalar ` W ) ) a ) ( .s ` W ) b ) = ( x ( .s ` W ) ( a ( .s ` W ) b ) ) )
51 5 sselda 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ x e. U ) -> x e. V )
52 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
53 2 12 15 52 lmodvs1 
 |-  ( ( W e. LMod /\ x e. V ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) x ) = x )
54 53 adantlr 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ x e. V ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) x ) = x )
55 51 54 syldan 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ x e. U ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) x ) = x )
56 8 11 14 17 18 19 20 21 23 26 29 38 47 50 55 islmodd 
 |-  ( ( W e. LMod /\ U e. S ) -> X e. LMod )
57 5 56 jca 
 |-  ( ( W e. LMod /\ U e. S ) -> ( U C_ V /\ X e. LMod ) )
58 simprl 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> U C_ V )
59 58 6 syl 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> U = ( Base ` X ) )
60 fvex 
 |-  ( Base ` X ) e. _V
61 59 60 eqeltrdi 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> U e. _V )
62 1 12 resssca 
 |-  ( U e. _V -> ( Scalar ` W ) = ( Scalar ` X ) )
63 61 62 syl 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> ( Scalar ` W ) = ( Scalar ` X ) )
64 63 eqcomd 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> ( Scalar ` X ) = ( Scalar ` W ) )
65 eqidd 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> ( Base ` ( Scalar ` X ) ) = ( Base ` ( Scalar ` X ) ) )
66 2 a1i 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> V = ( Base ` W ) )
67 1 9 ressplusg 
 |-  ( U e. _V -> ( +g ` W ) = ( +g ` X ) )
68 61 67 syl 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> ( +g ` W ) = ( +g ` X ) )
69 68 eqcomd 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> ( +g ` X ) = ( +g ` W ) )
70 1 15 ressvsca 
 |-  ( U e. _V -> ( .s ` W ) = ( .s ` X ) )
71 61 70 syl 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> ( .s ` W ) = ( .s ` X ) )
72 71 eqcomd 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> ( .s ` X ) = ( .s ` W ) )
73 3 a1i 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> S = ( LSubSp ` W ) )
74 59 58 eqsstrrd 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> ( Base ` X ) C_ V )
75 lmodgrp 
 |-  ( X e. LMod -> X e. Grp )
76 75 ad2antll 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> X e. Grp )
77 eqid 
 |-  ( Base ` X ) = ( Base ` X )
78 77 grpbn0 
 |-  ( X e. Grp -> ( Base ` X ) =/= (/) )
79 76 78 syl 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> ( Base ` X ) =/= (/) )
80 eqid 
 |-  ( LSubSp ` X ) = ( LSubSp ` X )
81 77 80 lss1 
 |-  ( X e. LMod -> ( Base ` X ) e. ( LSubSp ` X ) )
82 81 ad2antll 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> ( Base ` X ) e. ( LSubSp ` X ) )
83 eqid 
 |-  ( Scalar ` X ) = ( Scalar ` X )
84 eqid 
 |-  ( Base ` ( Scalar ` X ) ) = ( Base ` ( Scalar ` X ) )
85 eqid 
 |-  ( +g ` X ) = ( +g ` X )
86 eqid 
 |-  ( .s ` X ) = ( .s ` X )
87 83 84 85 86 80 lsscl 
 |-  ( ( ( Base ` X ) e. ( LSubSp ` X ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ a e. ( Base ` X ) /\ b e. ( Base ` X ) ) ) -> ( ( x ( .s ` X ) a ) ( +g ` X ) b ) e. ( Base ` X ) )
88 82 87 sylan 
 |-  ( ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) /\ ( x e. ( Base ` ( Scalar ` X ) ) /\ a e. ( Base ` X ) /\ b e. ( Base ` X ) ) ) -> ( ( x ( .s ` X ) a ) ( +g ` X ) b ) e. ( Base ` X ) )
89 64 65 66 69 72 73 74 79 88 islssd 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> ( Base ` X ) e. S )
90 59 89 eqeltrd 
 |-  ( ( W e. LMod /\ ( U C_ V /\ X e. LMod ) ) -> U e. S )
91 57 90 impbida 
 |-  ( W e. LMod -> ( U e. S <-> ( U C_ V /\ X e. LMod ) ) )