Metamath Proof Explorer

Theorem lclkrlem2c

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 } ) ) )
lclkrlem2c.j 
|- J = ( LSHyp ` U )
Assertion lclkrlem2c 
|- ( ph -> ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) .(+) ( N ` { B } ) ) e. J )

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 lclkrlem2c.j 
 |-  J = ( LSHyp ` U )
16 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
17 eqid 
 |-  ( ( joinH ` K ) ` W ) = ( ( joinH ` K ) ` W )
18 11 eldifad 
 |-  ( ph -> X e. V )
19 1 3 4 7 16 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
20 9 18 19 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
21 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
22 4 7 5 8 21 12 lsatlspsn 
 |-  ( ph -> ( N ` { Y } ) e. A )
23 1 16 3 6 8 9 20 22 dihsmatrn 
 |-  ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) e. ran ( ( DIsoH ` K ) ` W ) )
24 10 eldifad 
 |-  ( ph -> B e. V )
25 24 snssd 
 |-  ( ph -> { B } C_ V )
26 1 16 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { B } C_ V ) -> ( ._|_ ` { B } ) e. ran ( ( DIsoH ` K ) ` W ) )
27 9 25 26 syl2anc 
 |-  ( ph -> ( ._|_ ` { B } ) e. ran ( ( DIsoH ` K ) ` W ) )
28 1 16 3 4 2 17 9 23 27 dochdmm1 
 |-  ( ph -> ( ._|_ ` ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) ) = ( ( ._|_ ` ( ( N ` { X } ) .(+) ( N ` { Y } ) ) ) ( ( joinH ` K ) ` W ) ( ._|_ ` ( ._|_ ` { B } ) ) ) )
29 12 eldifad 
 |-  ( ph -> Y e. V )
30 4 7 6 21 18 29 lsmpr 
 |-  ( ph -> ( N ` { X , Y } ) = ( ( N ` { X } ) .(+) ( N ` { Y } ) ) )
31 df-pr 
 |-  { X , Y } = ( { X } u. { Y } )
32 31 fveq2i 
 |-  ( N ` { X , Y } ) = ( N ` ( { X } u. { Y } ) )
33 30 32 eqtr3di 
 |-  ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( N ` ( { X } u. { Y } ) ) )
34 33 fveq2d 
 |-  ( ph -> ( ._|_ ` ( ( N ` { X } ) .(+) ( N ` { Y } ) ) ) = ( ._|_ ` ( N ` ( { X } u. { Y } ) ) ) )
35 18 snssd 
 |-  ( ph -> { X } C_ V )
36 29 snssd 
 |-  ( ph -> { Y } C_ V )
37 35 36 unssd 
 |-  ( ph -> ( { X } u. { Y } ) C_ V )
38 1 3 2 4 7 9 37 dochocsp 
 |-  ( ph -> ( ._|_ ` ( N ` ( { X } u. { Y } ) ) ) = ( ._|_ ` ( { X } u. { Y } ) ) )
39 1 3 4 2 dochdmj1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { X } C_ V /\ { Y } C_ V ) -> ( ._|_ ` ( { X } u. { Y } ) ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
40 9 35 36 39 syl3anc 
 |-  ( ph -> ( ._|_ ` ( { X } u. { Y } ) ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
41 34 38 40 3eqtrd 
 |-  ( ph -> ( ._|_ ` ( ( N ` { X } ) .(+) ( N ` { Y } ) ) ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
42 1 3 2 4 7 9 24 dochocsn 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` { B } ) ) = ( N ` { B } ) )
43 41 42 oveq12d 
 |-  ( ph -> ( ( ._|_ ` ( ( N ` { X } ) .(+) ( N ` { Y } ) ) ) ( ( joinH ` K ) ` W ) ( ._|_ ` ( ._|_ ` { B } ) ) ) = ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) ( ( joinH ` K ) ` W ) ( N ` { B } ) ) )
44 1 16 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { X } C_ V ) -> ( ._|_ ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
45 9 35 44 syl2anc 
 |-  ( ph -> ( ._|_ ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
46 1 16 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { Y } C_ V ) -> ( ._|_ ` { Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
47 9 36 46 syl2anc 
 |-  ( ph -> ( ._|_ ` { Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
48 1 16 dihmeetcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ._|_ ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) /\ ( ._|_ ` { Y } ) e. ran ( ( DIsoH ` K ) ` W ) ) ) -> ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) e. ran ( ( DIsoH ` K ) ` W ) )
49 9 45 47 48 syl12anc 
 |-  ( ph -> ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) e. ran ( ( DIsoH ` K ) ` W ) )
50 1 3 4 6 7 16 17 9 49 24 dihjat1 
 |-  ( ph -> ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) ( ( joinH ` K ) ` W ) ( N ` { B } ) ) = ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) .(+) ( N ` { B } ) ) )
51 28 43 50 3eqtrrd 
 |-  ( ph -> ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) .(+) ( N ` { B } ) ) = ( ._|_ ` ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) ) )
52 1 2 3 4 5 6 7 8 9 10 11 12 13 14 lclkrlem2b 
 |-  ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) e. A )
53 1 3 2 8 15 9 52 dochsatshp 
 |-  ( ph -> ( ._|_ ` ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) ) e. J )
54 51 53 eqeltrd 
 |-  ( ph -> ( ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) .(+) ( N ` { B } ) ) e. J )