Metamath Proof Explorer

Theorem hdmap11lem1

Description: Lemma for hdmapadd . (Contributed by NM, 26-May-2015)

Ref Expression
Hypotheses hdmap11.h 
|- H = ( LHyp ` K )
hdmap11.u 
|- U = ( ( DVecH ` K ) ` W )
hdmap11.v 
|- V = ( Base ` U )
hdmap11.p 
|- .+ = ( +g ` U )
hdmap11.c 
|- C = ( ( LCDual ` K ) ` W )
hdmap11.a 
|- .+b = ( +g ` C )
hdmap11.s 
|- S = ( ( HDMap ` K ) ` W )
hdmap11.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmap11.x 
|- ( ph -> X e. V )
hdmap11.y 
|- ( ph -> Y e. V )
hdmap11.e 
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
hdmap11.o 
|- .0. = ( 0g ` U )
hdmap11.n 
|- N = ( LSpan ` U )
hdmap11.d 
|- D = ( Base ` C )
hdmap11.l 
|- L = ( LSpan ` C )
hdmap11.m 
|- M = ( ( mapd ` K ) ` W )
hdmap11.j 
|- J = ( ( HVMap ` K ) ` W )
hdmap11.i 
|- I = ( ( HDMap1 ` K ) ` W )
hdmap11lem0.1a 
|- ( ph -> z e. V )
hdmap11lem0.6 
|- ( ph -> -. z e. ( N ` { X , Y } ) )
hdmap11lem0.2a 
|- ( ph -> ( N ` { z } ) =/= ( N ` { E } ) )
Assertion hdmap11lem1 
|- ( ph -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )

Proof

Step Hyp Ref Expression
1 hdmap11.h 
 |-  H = ( LHyp ` K )
2 hdmap11.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmap11.v 
 |-  V = ( Base ` U )
4 hdmap11.p 
 |-  .+ = ( +g ` U )
5 hdmap11.c 
 |-  C = ( ( LCDual ` K ) ` W )
6 hdmap11.a 
 |-  .+b = ( +g ` C )
7 hdmap11.s 
 |-  S = ( ( HDMap ` K ) ` W )
8 hdmap11.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 hdmap11.x 
 |-  ( ph -> X e. V )
10 hdmap11.y 
 |-  ( ph -> Y e. V )
11 hdmap11.e 
 |-  E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
12 hdmap11.o 
 |-  .0. = ( 0g ` U )
13 hdmap11.n 
 |-  N = ( LSpan ` U )
14 hdmap11.d 
 |-  D = ( Base ` C )
15 hdmap11.l 
 |-  L = ( LSpan ` C )
16 hdmap11.m 
 |-  M = ( ( mapd ` K ) ` W )
17 hdmap11.j 
 |-  J = ( ( HVMap ` K ) ` W )
18 hdmap11.i 
 |-  I = ( ( HDMap1 ` K ) ` W )
19 hdmap11lem0.1a 
 |-  ( ph -> z e. V )
20 hdmap11lem0.6 
 |-  ( ph -> -. z e. ( N ` { X , Y } ) )
21 hdmap11lem0.2a 
 |-  ( ph -> ( N ` { z } ) =/= ( N ` { E } ) )
22 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
23 eqid 
 |-  ( Base ` K ) = ( Base ` K )
24 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
25 1 23 24 2 3 12 11 8 dvheveccl 
 |-  ( ph -> E e. ( V \ { .0. } ) )
26 1 2 3 12 5 14 22 17 8 25 hvmapcl2 
 |-  ( ph -> ( J ` E ) e. ( D \ { ( 0g ` C ) } ) )
27 26 eldifad 
 |-  ( ph -> ( J ` E ) e. D )
28 1 2 3 12 13 5 15 16 17 8 25 mapdhvmap 
 |-  ( ph -> ( M ` ( N ` { E } ) ) = ( L ` { ( J ` E ) } ) )
29 21 necomd 
 |-  ( ph -> ( N ` { E } ) =/= ( N ` { z } ) )
30 1 2 3 12 13 5 14 15 16 18 8 27 28 29 25 19 hdmap1cl 
 |-  ( ph -> ( I ` <. E , ( J ` E ) , z >. ) e. D )
31 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
32 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
33 3 31 13 32 9 10 lspprcl 
 |-  ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
34 12 31 32 33 19 20 lssneln0 
 |-  ( ph -> z e. ( V \ { .0. } ) )
35 eqidd 
 |-  ( ph -> ( I ` <. E , ( J ` E ) , z >. ) = ( I ` <. E , ( J ` E ) , z >. ) )
36 eqid 
 |-  ( -g ` U ) = ( -g ` U )
37 eqid 
 |-  ( -g ` C ) = ( -g ` C )
38 1 2 3 36 12 13 5 14 37 15 16 18 8 25 27 34 30 29 28 hdmap1eq 
 |-  ( ph -> ( ( I ` <. E , ( J ` E ) , z >. ) = ( I ` <. E , ( J ` E ) , z >. ) <-> ( ( M ` ( N ` { z } ) ) = ( L ` { ( I ` <. E , ( J ` E ) , z >. ) } ) /\ ( M ` ( N ` { ( E ( -g ` U ) z ) } ) ) = ( L ` { ( ( J ` E ) ( -g ` C ) ( I ` <. E , ( J ` E ) , z >. ) ) } ) ) ) )
39 35 38 mpbid 
 |-  ( ph -> ( ( M ` ( N ` { z } ) ) = ( L ` { ( I ` <. E , ( J ` E ) , z >. ) } ) /\ ( M ` ( N ` { ( E ( -g ` U ) z ) } ) ) = ( L ` { ( ( J ` E ) ( -g ` C ) ( I ` <. E , ( J ` E ) , z >. ) ) } ) ) )
40 39 simpld 
 |-  ( ph -> ( M ` ( N ` { z } ) ) = ( L ` { ( I ` <. E , ( J ` E ) , z >. ) } ) )
41 1 2 3 4 12 13 5 14 6 15 16 18 8 30 34 9 10 20 40 hdmap1l6 
 |-  ( ph -> ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , ( X .+ Y ) >. ) = ( ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , X >. ) .+b ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , Y >. ) ) )
42 3 4 lmodvacl 
 |-  ( ( U e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. V )
43 32 9 10 42 syl3anc 
 |-  ( ph -> ( X .+ Y ) e. V )
44 1 2 8 dvhlvec 
 |-  ( ph -> U e. LVec )
45 25 eldifad 
 |-  ( ph -> E e. V )
46 3 4 13 32 9 10 lspprvacl 
 |-  ( ph -> ( X .+ Y ) e. ( N ` { X , Y } ) )
47 31 13 32 33 46 lspsnel5a 
 |-  ( ph -> ( N ` { ( X .+ Y ) } ) C_ ( N ` { X , Y } ) )
48 47 20 ssneldd 
 |-  ( ph -> -. z e. ( N ` { ( X .+ Y ) } ) )
49 3 13 32 19 43 48 lspsnne2 
 |-  ( ph -> ( N ` { z } ) =/= ( N ` { ( X .+ Y ) } ) )
50 3 13 12 44 45 43 34 21 49 hdmaplem4 
 |-  ( ph -> -. z e. ( ( N ` { E } ) u. ( N ` { ( X .+ Y ) } ) ) )
51 1 11 2 3 13 5 14 17 18 7 8 43 19 50 hdmapval2 
 |-  ( ph -> ( S ` ( X .+ Y ) ) = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , ( X .+ Y ) >. ) )
52 3 13 44 19 9 10 20 lspindpi 
 |-  ( ph -> ( ( N ` { z } ) =/= ( N ` { X } ) /\ ( N ` { z } ) =/= ( N ` { Y } ) ) )
53 52 simpld 
 |-  ( ph -> ( N ` { z } ) =/= ( N ` { X } ) )
54 3 13 12 44 45 9 34 21 53 hdmaplem4 
 |-  ( ph -> -. z e. ( ( N ` { E } ) u. ( N ` { X } ) ) )
55 1 11 2 3 13 5 14 17 18 7 8 9 19 54 hdmapval2 
 |-  ( ph -> ( S ` X ) = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , X >. ) )
56 52 simprd 
 |-  ( ph -> ( N ` { z } ) =/= ( N ` { Y } ) )
57 3 13 12 44 45 10 34 21 56 hdmaplem4 
 |-  ( ph -> -. z e. ( ( N ` { E } ) u. ( N ` { Y } ) ) )
58 1 11 2 3 13 5 14 17 18 7 8 10 19 57 hdmapval2 
 |-  ( ph -> ( S ` Y ) = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , Y >. ) )
59 55 58 oveq12d 
 |-  ( ph -> ( ( S ` X ) .+b ( S ` Y ) ) = ( ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , X >. ) .+b ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , Y >. ) ) )
60 41 51 59 3eqtr4d 
 |-  ( ph -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )