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

Proof

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

Metamath Proof Explorer

Theorem lshpat

Proof