Metamath Proof Explorer

Theorem lclkrlem2d

Description: Lemma for lclkr . (Contributed by NM, 16-Jan-2015)

Ref Expression
Hypotheses lclkrlem2a.h 
|- H = ( LHyp ` K )
lclkrlem2a.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lclkrlem2a.u 
|- U = ( ( DVecH ` K ) ` W )
lclkrlem2a.v 
|- V = ( Base ` U )
lclkrlem2a.z 
|- .0. = ( 0g ` U )
lclkrlem2a.p 
|- .(+) = ( LSSum ` U )
lclkrlem2a.n 
|- N = ( LSpan ` U )
lclkrlem2a.a 
|- A = ( LSAtoms ` U )
lclkrlem2a.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lclkrlem2a.b 
|- ( ph -> B e. ( V \ { .0. } ) )
lclkrlem2a.x 
|- ( ph -> X e. ( V \ { .0. } ) )
lclkrlem2a.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
lclkrlem2a.e 
|- ( ph -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )
lclkrlem2b.da 
|- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )
lclkrlem2d.i 
|- I = ( ( DIsoH ` K ) ` W )
Assertion lclkrlem2d 
|- ( ph -> ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) .(+) ( N ` { B } ) ) e. ran I )

Proof

Step Hyp Ref Expression
1 lclkrlem2a.h 
 |-  H = ( LHyp ` K )
2 lclkrlem2a.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lclkrlem2a.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lclkrlem2a.v 
 |-  V = ( Base ` U )
5 lclkrlem2a.z 
 |-  .0. = ( 0g ` U )
6 lclkrlem2a.p 
 |-  .(+) = ( LSSum ` U )
7 lclkrlem2a.n 
 |-  N = ( LSpan ` U )
8 lclkrlem2a.a 
 |-  A = ( LSAtoms ` U )
9 lclkrlem2a.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 lclkrlem2a.b 
 |-  ( ph -> B e. ( V \ { .0. } ) )
11 lclkrlem2a.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
12 lclkrlem2a.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
13 lclkrlem2a.e 
 |-  ( ph -> ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) )
14 lclkrlem2b.da 
 |-  ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )
15 lclkrlem2d.i 
 |-  I = ( ( DIsoH ` K ) ` W )
16 11 eldifad 
 |-  ( ph -> X e. V )
17 16 snssd 
 |-  ( ph -> { X } C_ V )
18 1 15 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { X } C_ V ) -> ( ._|_ ` { X } ) e. ran I )
19 9 17 18 syl2anc 
 |-  ( ph -> ( ._|_ ` { X } ) e. ran I )
20 12 eldifad 
 |-  ( ph -> Y e. V )
21 20 snssd 
 |-  ( ph -> { Y } C_ V )
22 1 15 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { Y } C_ V ) -> ( ._|_ ` { Y } ) e. ran I )
23 9 21 22 syl2anc 
 |-  ( ph -> ( ._|_ ` { Y } ) e. ran I )
24 1 15 dihmeetcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ._|_ ` { X } ) e. ran I /\ ( ._|_ ` { Y } ) e. ran I ) ) -> ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) e. ran I )
25 9 19 23 24 syl12anc 
 |-  ( ph -> ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) e. ran I )
26 10 eldifad 
 |-  ( ph -> B e. V )
27 1 3 4 6 7 15 9 25 26 dihsmsprn 
 |-  ( ph -> ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) .(+) ( N ` { B } ) ) e. ran I )