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=LSubSpW
lshpat.p ˙=LSSumW
ishpat.h H=LSHypW
lshpat.a A=LSAtomsW
lshpat.w φWLVec
lshpat.l φUH
lshpat.q φQA
lshpat.r φRA
lshpat.n φQR
lshpat.m φ¬QU
Assertion lshpat φQ˙RUA

Proof

Step Hyp Ref Expression
1 lshpat.s S=LSubSpW
2 lshpat.p ˙=LSSumW
3 ishpat.h H=LSHypW
4 lshpat.a A=LSAtomsW
5 lshpat.w φWLVec
6 lshpat.l φUH
7 lshpat.q φQA
8 lshpat.r φRA
9 lshpat.n φQR
10 lshpat.m φ¬QU
11 eqid BaseW=BaseW
12 eqid LW=LW
13 11 1 3 12 5 islshpcv φUHUSULWBaseW
14 6 13 mpbid φUSULWBaseW
15 14 simpld φUS
16 14 simprd φULWBaseW
17 11 1 2 4 12 5 15 7 8 9 16 10 l1cvat φQ˙RUA