Metamath Proof Explorer


Theorem lshpat

Description: Create an atom under a hyperplane. Part of proof of Lemma B in Crawley p. 112. ( lhpat analog.) TODO: This changes U C V in l1cvpat and l1cvat to U e. H , which in turn change U e. H in islshpcv to U C V , with a couple of conversions of span to atom. Seems convoluted. Would a direct proof be better? (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses lshpat.s
|- S = ( LSubSp ` W )
lshpat.p
|- .(+) = ( LSSum ` W )
ishpat.h
|- H = ( LSHyp ` W )
lshpat.a
|- A = ( LSAtoms ` W )
lshpat.w
|- ( ph -> W e. LVec )
lshpat.l
|- ( ph -> U e. H )
lshpat.q
|- ( ph -> Q e. A )
lshpat.r
|- ( ph -> R e. A )
lshpat.n
|- ( ph -> Q =/= R )
lshpat.m
|- ( ph -> -. Q C_ U )
Assertion lshpat
|- ( ph -> ( ( Q .(+) R ) i^i U ) e. A )

Proof

Step Hyp Ref Expression
1 lshpat.s
 |-  S = ( LSubSp ` W )
2 lshpat.p
 |-  .(+) = ( LSSum ` W )
3 ishpat.h
 |-  H = ( LSHyp ` W )
4 lshpat.a
 |-  A = ( LSAtoms ` W )
5 lshpat.w
 |-  ( ph -> W e. LVec )
6 lshpat.l
 |-  ( ph -> U e. H )
7 lshpat.q
 |-  ( ph -> Q e. A )
8 lshpat.r
 |-  ( ph -> R e. A )
9 lshpat.n
 |-  ( ph -> Q =/= R )
10 lshpat.m
 |-  ( ph -> -. Q C_ U )
11 eqid
 |-  ( Base ` W ) = ( Base ` W )
12 eqid
 |-  ( 
    13 11 1 3 12 5 islshpcv
     |-  ( ph -> ( U e. H <-> ( U e. S /\ U ( 
      14 6 13 mpbid
       |-  ( ph -> ( U e. S /\ U ( 
        15 14 simpld
         |-  ( ph -> U e. S )
        16 14 simprd
         |-  ( ph -> U ( 
          17 11 1 2 4 12 5 15 7 8 9 16 10 l1cvat
           |-  ( ph -> ( ( Q .(+) R ) i^i U ) e. A )