Metamath Proof Explorer

Theorem mapdlsm

Description: Subspace sum is preserved by the map defined by df-mapd . Part of property (e) in Baer p. 40. (Contributed by NM, 13-Mar-2015)

Ref Expression
Hypotheses mapdlsm.h 
|- H = ( LHyp ` K )
mapdlsm.m 
|- M = ( ( mapd ` K ) ` W )
mapdlsm.u 
|- U = ( ( DVecH ` K ) ` W )
mapdlsm.s 
|- S = ( LSubSp ` U )
mapdlsm.p 
|- .(+) = ( LSSum ` U )
mapdlsm.c 
|- C = ( ( LCDual ` K ) ` W )
mapdlsm.q 
|- .+b = ( LSSum ` C )
mapdlsm.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
mapdlsm.x 
|- ( ph -> X e. S )
mapdlsm.y 
|- ( ph -> Y e. S )
Assertion mapdlsm 
|- ( ph -> ( M ` ( X .(+) Y ) ) = ( ( M ` X ) .+b ( M ` Y ) ) )

Proof

Step Hyp Ref Expression
1 mapdlsm.h 
 |-  H = ( LHyp ` K )
2 mapdlsm.m 
 |-  M = ( ( mapd ` K ) ` W )
3 mapdlsm.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 mapdlsm.s 
 |-  S = ( LSubSp ` U )
5 mapdlsm.p 
 |-  .(+) = ( LSSum ` U )
6 mapdlsm.c 
 |-  C = ( ( LCDual ` K ) ` W )
7 mapdlsm.q 
 |-  .+b = ( LSSum ` C )
8 mapdlsm.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 mapdlsm.x 
 |-  ( ph -> X e. S )
10 mapdlsm.y 
 |-  ( ph -> Y e. S )
11 1 6 8 lcdlmod 
 |-  ( ph -> C e. LMod )
12 eqid 
 |-  ( LSubSp ` C ) = ( LSubSp ` C )
13 12 lsssssubg 
 |-  ( C e. LMod -> ( LSubSp ` C ) C_ ( SubGrp ` C ) )
14 11 13 syl 
 |-  ( ph -> ( LSubSp ` C ) C_ ( SubGrp ` C ) )
15 1 2 3 4 6 12 8 9 mapdcl2 
 |-  ( ph -> ( M ` X ) e. ( LSubSp ` C ) )
16 14 15 sseldd 
 |-  ( ph -> ( M ` X ) e. ( SubGrp ` C ) )
17 1 2 3 4 6 12 8 10 mapdcl2 
 |-  ( ph -> ( M ` Y ) e. ( LSubSp ` C ) )
18 14 17 sseldd 
 |-  ( ph -> ( M ` Y ) e. ( SubGrp ` C ) )
19 7 lsmub1 
 |-  ( ( ( M ` X ) e. ( SubGrp ` C ) /\ ( M ` Y ) e. ( SubGrp ` C ) ) -> ( M ` X ) C_ ( ( M ` X ) .+b ( M ` Y ) ) )
20 16 18 19 syl2anc 
 |-  ( ph -> ( M ` X ) C_ ( ( M ` X ) .+b ( M ` Y ) ) )
21 1 2 3 4 8 9 mapdcl 
 |-  ( ph -> ( M ` X ) e. ran M )
22 1 2 3 4 8 10 mapdcl 
 |-  ( ph -> ( M ` Y ) e. ran M )
23 1 2 3 6 7 8 21 22 mapdlsmcl 
 |-  ( ph -> ( ( M ` X ) .+b ( M ` Y ) ) e. ran M )
24 1 2 8 23 mapdcnvid2 
 |-  ( ph -> ( M ` ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) = ( ( M ` X ) .+b ( M ` Y ) ) )
25 20 24 sseqtrrd 
 |-  ( ph -> ( M ` X ) C_ ( M ` ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) )
26 1 2 3 4 8 23 mapdcnvcl 
 |-  ( ph -> ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) e. S )
27 1 3 4 2 8 9 26 mapdord 
 |-  ( ph -> ( ( M ` X ) C_ ( M ` ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) <-> X C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) )
28 25 27 mpbid 
 |-  ( ph -> X C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) )
29 7 lsmub2 
 |-  ( ( ( M ` X ) e. ( SubGrp ` C ) /\ ( M ` Y ) e. ( SubGrp ` C ) ) -> ( M ` Y ) C_ ( ( M ` X ) .+b ( M ` Y ) ) )
30 16 18 29 syl2anc 
 |-  ( ph -> ( M ` Y ) C_ ( ( M ` X ) .+b ( M ` Y ) ) )
31 30 24 sseqtrrd 
 |-  ( ph -> ( M ` Y ) C_ ( M ` ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) )
32 1 3 4 2 8 10 26 mapdord 
 |-  ( ph -> ( ( M ` Y ) C_ ( M ` ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) <-> Y C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) )
33 31 32 mpbid 
 |-  ( ph -> Y C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) )
34 1 3 8 dvhlmod 
 |-  ( ph -> U e. LMod )
35 4 lsssssubg 
 |-  ( U e. LMod -> S C_ ( SubGrp ` U ) )
36 34 35 syl 
 |-  ( ph -> S C_ ( SubGrp ` U ) )
37 36 9 sseldd 
 |-  ( ph -> X e. ( SubGrp ` U ) )
38 36 10 sseldd 
 |-  ( ph -> Y e. ( SubGrp ` U ) )
39 36 26 sseldd 
 |-  ( ph -> ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) e. ( SubGrp ` U ) )
40 5 lsmlub 
 |-  ( ( X e. ( SubGrp ` U ) /\ Y e. ( SubGrp ` U ) /\ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) e. ( SubGrp ` U ) ) -> ( ( X C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) /\ Y C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) <-> ( X .(+) Y ) C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) )
41 37 38 39 40 syl3anc 
 |-  ( ph -> ( ( X C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) /\ Y C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) <-> ( X .(+) Y ) C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) )
42 28 33 41 mpbi2and 
 |-  ( ph -> ( X .(+) Y ) C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) )
43 4 5 lsmcl 
 |-  ( ( U e. LMod /\ X e. S /\ Y e. S ) -> ( X .(+) Y ) e. S )
44 34 9 10 43 syl3anc 
 |-  ( ph -> ( X .(+) Y ) e. S )
45 1 3 4 2 8 44 26 mapdord 
 |-  ( ph -> ( ( M ` ( X .(+) Y ) ) C_ ( M ` ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) <-> ( X .(+) Y ) C_ ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) )
46 42 45 mpbird 
 |-  ( ph -> ( M ` ( X .(+) Y ) ) C_ ( M ` ( `' M ` ( ( M ` X ) .+b ( M ` Y ) ) ) ) )
47 46 24 sseqtrd 
 |-  ( ph -> ( M ` ( X .(+) Y ) ) C_ ( ( M ` X ) .+b ( M ` Y ) ) )
48 5 lsmub1 
 |-  ( ( X e. ( SubGrp ` U ) /\ Y e. ( SubGrp ` U ) ) -> X C_ ( X .(+) Y ) )
49 37 38 48 syl2anc 
 |-  ( ph -> X C_ ( X .(+) Y ) )
50 1 3 4 2 8 9 44 mapdord 
 |-  ( ph -> ( ( M ` X ) C_ ( M ` ( X .(+) Y ) ) <-> X C_ ( X .(+) Y ) ) )
51 49 50 mpbird 
 |-  ( ph -> ( M ` X ) C_ ( M ` ( X .(+) Y ) ) )
52 5 lsmub2 
 |-  ( ( X e. ( SubGrp ` U ) /\ Y e. ( SubGrp ` U ) ) -> Y C_ ( X .(+) Y ) )
53 37 38 52 syl2anc 
 |-  ( ph -> Y C_ ( X .(+) Y ) )
54 1 3 4 2 8 10 44 mapdord 
 |-  ( ph -> ( ( M ` Y ) C_ ( M ` ( X .(+) Y ) ) <-> Y C_ ( X .(+) Y ) ) )
55 53 54 mpbird 
 |-  ( ph -> ( M ` Y ) C_ ( M ` ( X .(+) Y ) ) )
56 1 2 3 4 6 12 8 44 mapdcl2 
 |-  ( ph -> ( M ` ( X .(+) Y ) ) e. ( LSubSp ` C ) )
57 14 56 sseldd 
 |-  ( ph -> ( M ` ( X .(+) Y ) ) e. ( SubGrp ` C ) )
58 7 lsmlub 
 |-  ( ( ( M ` X ) e. ( SubGrp ` C ) /\ ( M ` Y ) e. ( SubGrp ` C ) /\ ( M ` ( X .(+) Y ) ) e. ( SubGrp ` C ) ) -> ( ( ( M ` X ) C_ ( M ` ( X .(+) Y ) ) /\ ( M ` Y ) C_ ( M ` ( X .(+) Y ) ) ) <-> ( ( M ` X ) .+b ( M ` Y ) ) C_ ( M ` ( X .(+) Y ) ) ) )
59 16 18 57 58 syl3anc 
 |-  ( ph -> ( ( ( M ` X ) C_ ( M ` ( X .(+) Y ) ) /\ ( M ` Y ) C_ ( M ` ( X .(+) Y ) ) ) <-> ( ( M ` X ) .+b ( M ` Y ) ) C_ ( M ` ( X .(+) Y ) ) ) )
60 51 55 59 mpbi2and 
 |-  ( ph -> ( ( M ` X ) .+b ( M ` Y ) ) C_ ( M ` ( X .(+) Y ) ) )
61 47 60 eqssd 
 |-  ( ph -> ( M ` ( X .(+) Y ) ) = ( ( M ` X ) .+b ( M ` Y ) ) )