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=\mathrm{LSubSp}\left(W\right)$$
	lshpat.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	ishpat.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
	lshpat.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lshpat.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lshpat.l	$$⊢\phi \to U\in H$$
	lshpat.q	$$⊢\phi \to Q\in A$$
	lshpat.r	$$⊢\phi \to R\in A$$
	lshpat.n	$$⊢\phi \to Q\ne R$$
	lshpat.m	$$⊢\phi \to \neg Q\subseteq U$$
Assertion	lshpat	$$⊢\phi \to \left(Q\underset{\dot{}}{\oplus }R\right)\cap U\in A$$

Proof

Step	Hyp	Ref	Expression
1		lshpat.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lshpat.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
3		ishpat.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
4		lshpat.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
5		lshpat.w	$$⊢\phi \to W\in \mathrm{LVec}$$
6		lshpat.l	$$⊢\phi \to U\in H$$
7		lshpat.q	$$⊢\phi \to Q\in A$$
8		lshpat.r	$$⊢\phi \to R\in A$$
9		lshpat.n	$$⊢\phi \to Q\ne R$$
10		lshpat.m	$$⊢\phi \to \neg Q\subseteq U$$
11		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
12		eqid	$$⊢{⋖}_L\left(W\right)={⋖}_L\left(W\right)$$
13	11 1 3 12 5	islshpcv	$$⊢\phi \to \left(U\in H\leftrightarrow \left(U\in S\wedge U{⋖}_L\left(W\right){\mathrm{Base}}_W\right)\right)$$
14	6 13	mpbid	$$⊢\phi \to \left(U\in S\wedge U{⋖}_L\left(W\right){\mathrm{Base}}_W\right)$$
15	14	simpld	$$⊢\phi \to U\in S$$
16	14	simprd	$$⊢\phi \to U{⋖}_L\left(W\right){\mathrm{Base}}_W$$
17	11 1 2 4 12 5 15 7 8 9 16 10	l1cvat	$$⊢\phi \to \left(Q\underset{\dot{}}{\oplus }R\right)\cap U\in A$$