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 )

Metamath Proof Explorer

Theorem lshpat

Proof