Metamath Proof Explorer

Theorem lclkrlem2a

Description: Lemma for lclkr . Use lshpat to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (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 } ) )
lclkrlem2a.d 
|- ( ph -> -. X e. ( ._|_ ` { B } ) )
Assertion lclkrlem2a 
|- ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) e. A )

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 lclkrlem2a.d 
 |-  ( ph -> -. X e. ( ._|_ ` { B } ) )
15 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
16 eqid 
 |-  ( LSHyp ` U ) = ( LSHyp ` U )
17 1 3 9 dvhlvec 
 |-  ( ph -> U e. LVec )
18 1 2 3 4 5 16 9 10 dochsnshp 
 |-  ( ph -> ( ._|_ ` { B } ) e. ( LSHyp ` U ) )
19 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
20 4 7 5 8 19 11 lsatlspsn 
 |-  ( ph -> ( N ` { X } ) e. A )
21 4 7 5 8 19 12 lsatlspsn 
 |-  ( ph -> ( N ` { Y } ) e. A )
22 11 eldifad 
 |-  ( ph -> X e. V )
23 22 snssd 
 |-  ( ph -> { X } C_ V )
24 1 3 2 4 7 9 23 dochocsp 
 |-  ( ph -> ( ._|_ ` ( N ` { X } ) ) = ( ._|_ ` { X } ) )
25 12 eldifad 
 |-  ( ph -> Y e. V )
26 25 snssd 
 |-  ( ph -> { Y } C_ V )
27 1 3 2 4 7 9 26 dochocsp 
 |-  ( ph -> ( ._|_ ` ( N ` { Y } ) ) = ( ._|_ ` { Y } ) )
28 24 27 eqeq12d 
 |-  ( ph -> ( ( ._|_ ` ( N ` { X } ) ) = ( ._|_ ` ( N ` { Y } ) ) <-> ( ._|_ ` { X } ) = ( ._|_ ` { Y } ) ) )
29 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
30 1 3 4 7 29 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
31 9 22 30 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
32 1 3 4 7 29 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. V ) -> ( N ` { Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
33 9 25 32 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ran ( ( DIsoH ` K ) ` W ) )
34 1 29 2 9 31 33 doch11 
 |-  ( ph -> ( ( ._|_ ` ( N ` { X } ) ) = ( ._|_ ` ( N ` { Y } ) ) <-> ( N ` { X } ) = ( N ` { Y } ) ) )
35 28 34 bitr3d 
 |-  ( ph -> ( ( ._|_ ` { X } ) = ( ._|_ ` { Y } ) <-> ( N ` { X } ) = ( N ` { Y } ) ) )
36 35 necon3bid 
 |-  ( ph -> ( ( ._|_ ` { X } ) =/= ( ._|_ ` { Y } ) <-> ( N ` { X } ) =/= ( N ` { Y } ) ) )
37 13 36 mpbid 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
38 10 eldifad 
 |-  ( ph -> B e. V )
39 38 snssd 
 |-  ( ph -> { B } C_ V )
40 1 3 4 15 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { B } C_ V ) -> ( ._|_ ` { B } ) e. ( LSubSp ` U ) )
41 9 39 40 syl2anc 
 |-  ( ph -> ( ._|_ ` { B } ) e. ( LSubSp ` U ) )
42 4 15 7 19 41 22 ellspsn5b 
 |-  ( ph -> ( X e. ( ._|_ ` { B } ) <-> ( N ` { X } ) C_ ( ._|_ ` { B } ) ) )
43 14 42 mtbid 
 |-  ( ph -> -. ( N ` { X } ) C_ ( ._|_ ` { B } ) )
44 15 6 16 8 17 18 20 21 37 43 lshpat 
 |-  ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) i^i ( ._|_ ` { B } ) ) e. A )