Metamath Proof Explorer

Theorem hdmap11lem2

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 )
Assertion hdmap11lem2 
|- ( 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 1 2 3 13 8 9 10 dvh3dim 
 |-  ( ph -> E. z e. V -. z e. ( N ` { X , Y } ) )
20 19 adantr 
 |-  ( ( ph /\ E e. ( N ` { X , Y } ) ) -> E. z e. V -. z e. ( N ` { X , Y } ) )
21 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
22 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
23 22 adantr 
 |-  ( ( ph /\ E e. ( N ` { X , Y } ) ) -> U e. LMod )
24 3 21 13 22 9 10 lspprcl 
 |-  ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
25 24 adantr 
 |-  ( ( ph /\ E e. ( N ` { X , Y } ) ) -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
26 simpr 
 |-  ( ( ph /\ E e. ( N ` { X , Y } ) ) -> E e. ( N ` { X , Y } ) )
27 21 13 23 25 26 ellspsn5 
 |-  ( ( ph /\ E e. ( N ` { X , Y } ) ) -> ( N ` { E } ) C_ ( N ` { X , Y } ) )
28 27 ssneld 
 |-  ( ( ph /\ E e. ( N ` { X , Y } ) ) -> ( -. z e. ( N ` { X , Y } ) -> -. z e. ( N ` { E } ) ) )
29 28 ancld 
 |-  ( ( ph /\ E e. ( N ` { X , Y } ) ) -> ( -. z e. ( N ` { X , Y } ) -> ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) )
30 29 reximdv 
 |-  ( ( ph /\ E e. ( N ` { X , Y } ) ) -> ( E. z e. V -. z e. ( N ` { X , Y } ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) )
31 20 30 mpd 
 |-  ( ( ph /\ E e. ( N ` { X , Y } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) )
32 eqid 
 |-  ( Base ` K ) = ( Base ` K )
33 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
34 1 32 33 2 3 12 11 8 dvheveccl 
 |-  ( ph -> E e. ( V \ { .0. } ) )
35 34 eldifad 
 |-  ( ph -> E e. V )
36 1 2 3 13 8 35 10 dvh3dim 
 |-  ( ph -> E. z e. V -. z e. ( N ` { E , Y } ) )
37 36 adantr 
 |-  ( ( ph /\ X = .0. ) -> E. z e. V -. z e. ( N ` { E , Y } ) )
38 preq1 
 |-  ( X = .0. -> { X , Y } = { .0. , Y } )
39 prcom 
 |-  { .0. , Y } = { Y , .0. }
40 38 39 eqtrdi 
 |-  ( X = .0. -> { X , Y } = { Y , .0. } )
41 40 fveq2d 
 |-  ( X = .0. -> ( N ` { X , Y } ) = ( N ` { Y , .0. } ) )
42 3 12 13 22 10 lsppr0 
 |-  ( ph -> ( N ` { Y , .0. } ) = ( N ` { Y } ) )
43 41 42 sylan9eqr 
 |-  ( ( ph /\ X = .0. ) -> ( N ` { X , Y } ) = ( N ` { Y } ) )
44 3 21 13 22 35 10 lspprcl 
 |-  ( ph -> ( N ` { E , Y } ) e. ( LSubSp ` U ) )
45 3 13 22 35 10 lspprid2 
 |-  ( ph -> Y e. ( N ` { E , Y } ) )
46 21 13 22 44 45 ellspsn5 
 |-  ( ph -> ( N ` { Y } ) C_ ( N ` { E , Y } ) )
47 46 adantr 
 |-  ( ( ph /\ X = .0. ) -> ( N ` { Y } ) C_ ( N ` { E , Y } ) )
48 43 47 eqsstrd 
 |-  ( ( ph /\ X = .0. ) -> ( N ` { X , Y } ) C_ ( N ` { E , Y } ) )
49 48 ssneld 
 |-  ( ( ph /\ X = .0. ) -> ( -. z e. ( N ` { E , Y } ) -> -. z e. ( N ` { X , Y } ) ) )
50 3 13 22 35 10 lspprid1 
 |-  ( ph -> E e. ( N ` { E , Y } ) )
51 21 13 22 44 50 ellspsn5 
 |-  ( ph -> ( N ` { E } ) C_ ( N ` { E , Y } ) )
52 51 adantr 
 |-  ( ( ph /\ X = .0. ) -> ( N ` { E } ) C_ ( N ` { E , Y } ) )
53 52 ssneld 
 |-  ( ( ph /\ X = .0. ) -> ( -. z e. ( N ` { E , Y } ) -> -. z e. ( N ` { E } ) ) )
54 49 53 jcad 
 |-  ( ( ph /\ X = .0. ) -> ( -. z e. ( N ` { E , Y } ) -> ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) )
55 54 reximdv 
 |-  ( ( ph /\ X = .0. ) -> ( E. z e. V -. z e. ( N ` { E , Y } ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) )
56 37 55 mpd 
 |-  ( ( ph /\ X = .0. ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) )
57 56 adantlr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X = .0. ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) )
58 3 4 lmodvacl 
 |-  ( ( U e. LMod /\ E e. V /\ X e. V ) -> ( E .+ X ) e. V )
59 22 35 9 58 syl3anc 
 |-  ( ph -> ( E .+ X ) e. V )
60 59 ad2antrr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> ( E .+ X ) e. V )
61 22 ad2antrr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> U e. LMod )
62 24 ad2antrr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
63 3 13 22 9 10 lspprid1 
 |-  ( ph -> X e. ( N ` { X , Y } ) )
64 63 ad2antrr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> X e. ( N ` { X , Y } ) )
65 35 ad2antrr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> E e. V )
66 simplr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> -. E e. ( N ` { X , Y } ) )
67 3 4 21 61 62 64 65 66 lssvancl2 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> -. ( E .+ X ) e. ( N ` { X , Y } ) )
68 3 21 13 lspsncl 
 |-  ( ( U e. LMod /\ E e. V ) -> ( N ` { E } ) e. ( LSubSp ` U ) )
69 22 35 68 syl2anc 
 |-  ( ph -> ( N ` { E } ) e. ( LSubSp ` U ) )
70 69 ad2antrr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> ( N ` { E } ) e. ( LSubSp ` U ) )
71 3 13 lspsnid 
 |-  ( ( U e. LMod /\ E e. V ) -> E e. ( N ` { E } ) )
72 22 35 71 syl2anc 
 |-  ( ph -> E e. ( N ` { E } ) )
73 72 ad2antrr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> E e. ( N ` { E } ) )
74 9 ad2antrr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> X e. V )
75 1 2 8 dvhlvec 
 |-  ( ph -> U e. LVec )
76 75 ad2antrr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> U e. LVec )
77 simpr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> X =/= .0. )
78 eldifsn 
 |-  ( X e. ( V \ { .0. } ) <-> ( X e. V /\ X =/= .0. ) )
79 74 77 78 sylanbrc 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> X e. ( V \ { .0. } ) )
80 21 13 22 24 63 ellspsn5 
 |-  ( ph -> ( N ` { X } ) C_ ( N ` { X , Y } ) )
81 80 sseld 
 |-  ( ph -> ( E e. ( N ` { X } ) -> E e. ( N ` { X , Y } ) ) )
82 81 con3dimp 
 |-  ( ( ph /\ -. E e. ( N ` { X , Y } ) ) -> -. E e. ( N ` { X } ) )
83 82 adantr 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> -. E e. ( N ` { X } ) )
84 3 12 13 76 65 79 83 lspsnnecom 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> -. X e. ( N ` { E } ) )
85 3 4 21 61 70 73 74 84 lssvancl1 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> -. ( E .+ X ) e. ( N ` { E } ) )
86 eleq1 
 |-  ( z = ( E .+ X ) -> ( z e. ( N ` { X , Y } ) <-> ( E .+ X ) e. ( N ` { X , Y } ) ) )
87 86 notbid 
 |-  ( z = ( E .+ X ) -> ( -. z e. ( N ` { X , Y } ) <-> -. ( E .+ X ) e. ( N ` { X , Y } ) ) )
88 eleq1 
 |-  ( z = ( E .+ X ) -> ( z e. ( N ` { E } ) <-> ( E .+ X ) e. ( N ` { E } ) ) )
89 88 notbid 
 |-  ( z = ( E .+ X ) -> ( -. z e. ( N ` { E } ) <-> -. ( E .+ X ) e. ( N ` { E } ) ) )
90 87 89 anbi12d 
 |-  ( z = ( E .+ X ) -> ( ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) <-> ( -. ( E .+ X ) e. ( N ` { X , Y } ) /\ -. ( E .+ X ) e. ( N ` { E } ) ) ) )
91 90 rspcev 
 |-  ( ( ( E .+ X ) e. V /\ ( -. ( E .+ X ) e. ( N ` { X , Y } ) /\ -. ( E .+ X ) e. ( N ` { E } ) ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) )
92 60 67 85 91 syl12anc 
 |-  ( ( ( ph /\ -. E e. ( N ` { X , Y } ) ) /\ X =/= .0. ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) )
93 57 92 pm2.61dane 
 |-  ( ( ph /\ -. E e. ( N ` { X , Y } ) ) -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) )
94 31 93 pm2.61dan 
 |-  ( ph -> E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) )
95 8 3ad2ant1 
 |-  ( ( ph /\ z e. V /\ ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) -> ( K e. HL /\ W e. H ) )
96 9 3ad2ant1 
 |-  ( ( ph /\ z e. V /\ ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) -> X e. V )
97 10 3ad2ant1 
 |-  ( ( ph /\ z e. V /\ ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) -> Y e. V )
98 simp2 
 |-  ( ( ph /\ z e. V /\ ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) -> z e. V )
99 simp3l 
 |-  ( ( ph /\ z e. V /\ ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) -> -. z e. ( N ` { X , Y } ) )
100 22 3ad2ant1 
 |-  ( ( ph /\ z e. V /\ ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) -> U e. LMod )
101 35 3ad2ant1 
 |-  ( ( ph /\ z e. V /\ ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) -> E e. V )
102 simp3r 
 |-  ( ( ph /\ z e. V /\ ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) -> -. z e. ( N ` { E } ) )
103 3 13 100 98 101 102 lspsnne2 
 |-  ( ( ph /\ z e. V /\ ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) -> ( N ` { z } ) =/= ( N ` { E } ) )
104 1 2 3 4 5 6 7 95 96 97 11 12 13 14 15 16 17 18 98 99 103 hdmap11lem1 
 |-  ( ( ph /\ z e. V /\ ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) ) -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )
105 104 rexlimdv3a 
 |-  ( ph -> ( E. z e. V ( -. z e. ( N ` { X , Y } ) /\ -. z e. ( N ` { E } ) ) -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) ) )
106 94 105 mpd 
 |-  ( ph -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )