Metamath Proof Explorer

Theorem lsmcl

Description: The sum of two subspaces is a subspace. (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmcl.s 
|- S = ( LSubSp ` W )
lsmcl.p 
|- .(+) = ( LSSum ` W )
Assertion lsmcl 
|- ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T .(+) U ) e. S )

Proof

Step Hyp Ref Expression
1 lsmcl.s 
 |-  S = ( LSubSp ` W )
2 lsmcl.p 
 |-  .(+) = ( LSSum ` W )
3 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
4 3 3ad2ant1 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> W e. Abel )
5 1 lsssubg 
 |-  ( ( W e. LMod /\ T e. S ) -> T e. ( SubGrp ` W ) )
6 5 3adant3 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> T e. ( SubGrp ` W ) )
7 1 lsssubg 
 |-  ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) )
8 7 3adant2 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> U e. ( SubGrp ` W ) )
9 2 lsmsubg2 
 |-  ( ( W e. Abel /\ T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( T .(+) U ) e. ( SubGrp ` W ) )
10 4 6 8 9 syl3anc 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T .(+) U ) e. ( SubGrp ` W ) )
11 eqid 
 |-  ( +g ` W ) = ( +g ` W )
12 11 2 lsmelval 
 |-  ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( u e. ( T .(+) U ) <-> E. d e. T E. e e. U u = ( d ( +g ` W ) e ) ) )
13 6 8 12 syl2anc 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( u e. ( T .(+) U ) <-> E. d e. T E. e e. U u = ( d ( +g ` W ) e ) ) )
14 13 adantr 
 |-  ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) -> ( u e. ( T .(+) U ) <-> E. d e. T E. e e. U u = ( d ( +g ` W ) e ) ) )
15 simpll1 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> W e. LMod )
16 simplr 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> a e. ( Base ` ( Scalar ` W ) ) )
17 simpll2 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> T e. S )
18 simprl 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> d e. T )
19 eqid 
 |-  ( Base ` W ) = ( Base ` W )
20 19 1 lssel 
 |-  ( ( T e. S /\ d e. T ) -> d e. ( Base ` W ) )
21 17 18 20 syl2anc 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> d e. ( Base ` W ) )
22 simpll3 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> U e. S )
23 simprr 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> e e. U )
24 19 1 lssel 
 |-  ( ( U e. S /\ e e. U ) -> e e. ( Base ` W ) )
25 22 23 24 syl2anc 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> e e. ( Base ` W ) )
26 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
27 eqid 
 |-  ( .s ` W ) = ( .s ` W )
28 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
29 19 11 26 27 28 lmodvsdi 
 |-  ( ( W e. LMod /\ ( a e. ( Base ` ( Scalar ` W ) ) /\ d e. ( Base ` W ) /\ e e. ( Base ` W ) ) ) -> ( a ( .s ` W ) ( d ( +g ` W ) e ) ) = ( ( a ( .s ` W ) d ) ( +g ` W ) ( a ( .s ` W ) e ) ) )
30 15 16 21 25 29 syl13anc 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> ( a ( .s ` W ) ( d ( +g ` W ) e ) ) = ( ( a ( .s ` W ) d ) ( +g ` W ) ( a ( .s ` W ) e ) ) )
31 15 17 5 syl2anc 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> T e. ( SubGrp ` W ) )
32 15 22 7 syl2anc 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> U e. ( SubGrp ` W ) )
33 26 27 28 1 lssvscl 
 |-  ( ( ( W e. LMod /\ T e. S ) /\ ( a e. ( Base ` ( Scalar ` W ) ) /\ d e. T ) ) -> ( a ( .s ` W ) d ) e. T )
34 15 17 16 18 33 syl22anc 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> ( a ( .s ` W ) d ) e. T )
35 26 27 28 1 lssvscl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( a e. ( Base ` ( Scalar ` W ) ) /\ e e. U ) ) -> ( a ( .s ` W ) e ) e. U )
36 15 22 16 23 35 syl22anc 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> ( a ( .s ` W ) e ) e. U )
37 11 2 lsmelvali 
 |-  ( ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) /\ ( ( a ( .s ` W ) d ) e. T /\ ( a ( .s ` W ) e ) e. U ) ) -> ( ( a ( .s ` W ) d ) ( +g ` W ) ( a ( .s ` W ) e ) ) e. ( T .(+) U ) )
38 31 32 34 36 37 syl22anc 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> ( ( a ( .s ` W ) d ) ( +g ` W ) ( a ( .s ` W ) e ) ) e. ( T .(+) U ) )
39 30 38 eqeltrd 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> ( a ( .s ` W ) ( d ( +g ` W ) e ) ) e. ( T .(+) U ) )
40 oveq2 
 |-  ( u = ( d ( +g ` W ) e ) -> ( a ( .s ` W ) u ) = ( a ( .s ` W ) ( d ( +g ` W ) e ) ) )
41 40 eleq1d 
 |-  ( u = ( d ( +g ` W ) e ) -> ( ( a ( .s ` W ) u ) e. ( T .(+) U ) <-> ( a ( .s ` W ) ( d ( +g ` W ) e ) ) e. ( T .(+) U ) ) )
42 39 41 syl5ibrcom 
 |-  ( ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) /\ ( d e. T /\ e e. U ) ) -> ( u = ( d ( +g ` W ) e ) -> ( a ( .s ` W ) u ) e. ( T .(+) U ) ) )
43 42 rexlimdvva 
 |-  ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) -> ( E. d e. T E. e e. U u = ( d ( +g ` W ) e ) -> ( a ( .s ` W ) u ) e. ( T .(+) U ) ) )
44 14 43 sylbid 
 |-  ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ a e. ( Base ` ( Scalar ` W ) ) ) -> ( u e. ( T .(+) U ) -> ( a ( .s ` W ) u ) e. ( T .(+) U ) ) )
45 44 impr 
 |-  ( ( ( W e. LMod /\ T e. S /\ U e. S ) /\ ( a e. ( Base ` ( Scalar ` W ) ) /\ u e. ( T .(+) U ) ) ) -> ( a ( .s ` W ) u ) e. ( T .(+) U ) )
46 45 ralrimivva 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> A. a e. ( Base ` ( Scalar ` W ) ) A. u e. ( T .(+) U ) ( a ( .s ` W ) u ) e. ( T .(+) U ) )
47 26 28 19 27 1 islss4 
 |-  ( W e. LMod -> ( ( T .(+) U ) e. S <-> ( ( T .(+) U ) e. ( SubGrp ` W ) /\ A. a e. ( Base ` ( Scalar ` W ) ) A. u e. ( T .(+) U ) ( a ( .s ` W ) u ) e. ( T .(+) U ) ) ) )
48 47 3ad2ant1 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( ( T .(+) U ) e. S <-> ( ( T .(+) U ) e. ( SubGrp ` W ) /\ A. a e. ( Base ` ( Scalar ` W ) ) A. u e. ( T .(+) U ) ( a ( .s ` W ) u ) e. ( T .(+) U ) ) ) )
49 10 46 48 mpbir2and 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T .(+) U ) e. S )