Metamath Proof Explorer

Theorem mapdin

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

Ref Expression
Hypotheses mapdin.h 
|- H = ( LHyp ` K )
mapdin.m 
|- M = ( ( mapd ` K ) ` W )
mapdin.u 
|- U = ( ( DVecH ` K ) ` W )
mapdin.s 
|- S = ( LSubSp ` U )
mapdin.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
mapdin.x 
|- ( ph -> X e. S )
mapdin.y 
|- ( ph -> Y e. S )
Assertion mapdin 
|- ( ph -> ( M ` ( X i^i Y ) ) = ( ( M ` X ) i^i ( M ` Y ) ) )

Proof

Step Hyp Ref Expression
1 mapdin.h 
 |-  H = ( LHyp ` K )
2 mapdin.m 
 |-  M = ( ( mapd ` K ) ` W )
3 mapdin.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 mapdin.s 
 |-  S = ( LSubSp ` U )
5 mapdin.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
6 mapdin.x 
 |-  ( ph -> X e. S )
7 mapdin.y 
 |-  ( ph -> Y e. S )
8 inss1 
 |-  ( X i^i Y ) C_ X
9 1 3 5 dvhlmod 
 |-  ( ph -> U e. LMod )
10 4 lssincl 
 |-  ( ( U e. LMod /\ X e. S /\ Y e. S ) -> ( X i^i Y ) e. S )
11 9 6 7 10 syl3anc 
 |-  ( ph -> ( X i^i Y ) e. S )
12 1 3 4 2 5 11 6 mapdord 
 |-  ( ph -> ( ( M ` ( X i^i Y ) ) C_ ( M ` X ) <-> ( X i^i Y ) C_ X ) )
13 8 12 mpbiri 
 |-  ( ph -> ( M ` ( X i^i Y ) ) C_ ( M ` X ) )
14 inss2 
 |-  ( X i^i Y ) C_ Y
15 1 3 4 2 5 11 7 mapdord 
 |-  ( ph -> ( ( M ` ( X i^i Y ) ) C_ ( M ` Y ) <-> ( X i^i Y ) C_ Y ) )
16 14 15 mpbiri 
 |-  ( ph -> ( M ` ( X i^i Y ) ) C_ ( M ` Y ) )
17 13 16 ssind 
 |-  ( ph -> ( M ` ( X i^i Y ) ) C_ ( ( M ` X ) i^i ( M ` Y ) ) )
18 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
19 eqid 
 |-  ( LSubSp ` ( ( LCDual ` K ) ` W ) ) = ( LSubSp ` ( ( LCDual ` K ) ` W ) )
20 1 2 3 4 18 19 5 6 mapdcl2 
 |-  ( ph -> ( M ` X ) e. ( LSubSp ` ( ( LCDual ` K ) ` W ) ) )
21 1 2 18 19 5 mapdrn2 
 |-  ( ph -> ran M = ( LSubSp ` ( ( LCDual ` K ) ` W ) ) )
22 20 21 eleqtrrd 
 |-  ( ph -> ( M ` X ) e. ran M )
23 1 2 3 4 18 19 5 7 mapdcl2 
 |-  ( ph -> ( M ` Y ) e. ( LSubSp ` ( ( LCDual ` K ) ` W ) ) )
24 23 21 eleqtrrd 
 |-  ( ph -> ( M ` Y ) e. ran M )
25 1 2 3 18 5 22 24 mapdincl 
 |-  ( ph -> ( ( M ` X ) i^i ( M ` Y ) ) e. ran M )
26 1 2 5 25 mapdcnvid2 
 |-  ( ph -> ( M ` ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) ) = ( ( M ` X ) i^i ( M ` Y ) ) )
27 inss1 
 |-  ( ( M ` X ) i^i ( M ` Y ) ) C_ ( M ` X )
28 26 27 eqsstrdi 
 |-  ( ph -> ( M ` ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) ) C_ ( M ` X ) )
29 1 18 5 lcdlmod 
 |-  ( ph -> ( ( LCDual ` K ) ` W ) e. LMod )
30 19 lssincl 
 |-  ( ( ( ( LCDual ` K ) ` W ) e. LMod /\ ( M ` X ) e. ( LSubSp ` ( ( LCDual ` K ) ` W ) ) /\ ( M ` Y ) e. ( LSubSp ` ( ( LCDual ` K ) ` W ) ) ) -> ( ( M ` X ) i^i ( M ` Y ) ) e. ( LSubSp ` ( ( LCDual ` K ) ` W ) ) )
31 29 20 23 30 syl3anc 
 |-  ( ph -> ( ( M ` X ) i^i ( M ` Y ) ) e. ( LSubSp ` ( ( LCDual ` K ) ` W ) ) )
32 31 21 eleqtrrd 
 |-  ( ph -> ( ( M ` X ) i^i ( M ` Y ) ) e. ran M )
33 1 2 3 4 5 32 mapdcnvcl 
 |-  ( ph -> ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) e. S )
34 1 3 4 2 5 33 6 mapdord 
 |-  ( ph -> ( ( M ` ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) ) C_ ( M ` X ) <-> ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) C_ X ) )
35 28 34 mpbid 
 |-  ( ph -> ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) C_ X )
36 1 2 5 32 mapdcnvid2 
 |-  ( ph -> ( M ` ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) ) = ( ( M ` X ) i^i ( M ` Y ) ) )
37 inss2 
 |-  ( ( M ` X ) i^i ( M ` Y ) ) C_ ( M ` Y )
38 36 37 eqsstrdi 
 |-  ( ph -> ( M ` ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) ) C_ ( M ` Y ) )
39 1 3 4 2 5 33 7 mapdord 
 |-  ( ph -> ( ( M ` ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) ) C_ ( M ` Y ) <-> ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) C_ Y ) )
40 38 39 mpbid 
 |-  ( ph -> ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) C_ Y )
41 35 40 ssind 
 |-  ( ph -> ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) C_ ( X i^i Y ) )
42 1 3 4 2 5 33 11 mapdord 
 |-  ( ph -> ( ( M ` ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) ) C_ ( M ` ( X i^i Y ) ) <-> ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) C_ ( X i^i Y ) ) )
43 41 42 mpbird 
 |-  ( ph -> ( M ` ( `' M ` ( ( M ` X ) i^i ( M ` Y ) ) ) ) C_ ( M ` ( X i^i Y ) ) )
44 26 43 eqsstrrd 
 |-  ( ph -> ( ( M ` X ) i^i ( M ` Y ) ) C_ ( M ` ( X i^i Y ) ) )
45 17 44 eqssd 
 |-  ( ph -> ( M ` ( X i^i Y ) ) = ( ( M ` X ) i^i ( M ` Y ) ) )