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	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lshpat.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	ishpat.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
	lshpat.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lshpat.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lshpat.l	⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
	lshpat.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
	lshpat.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
	lshpat.n	⊢ ( 𝜑 → 𝑄 ≠ 𝑅 )
	lshpat.m	⊢ ( 𝜑 → ¬ 𝑄 ⊆ 𝑈 )
Assertion	lshpat	⊢ ( 𝜑 → ( ( 𝑄 ⊕ 𝑅 ) ∩ 𝑈 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		lshpat.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lshpat.p	⊢ ⊕ = ( LSSum ‘ 𝑊 )
3		ishpat.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
4		lshpat.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5		lshpat.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lshpat.l	⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
7		lshpat.q	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8		lshpat.r	⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
9		lshpat.n	⊢ ( 𝜑 → 𝑄 ≠ 𝑅 )
10		lshpat.m	⊢ ( 𝜑 → ¬ 𝑄 ⊆ 𝑈 )
11		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12		eqid	⊢ ( ⋖L ‘ 𝑊 ) = ( ⋖L ‘ 𝑊 )
13	11 1 3 12 5	islshpcv	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ 𝑆 ∧ 𝑈 ( ⋖L ‘ 𝑊 ) ( Base ‘ 𝑊 ) ) ) )
14	6 13	mpbid	⊢ ( 𝜑 → ( 𝑈 ∈ 𝑆 ∧ 𝑈 ( ⋖L ‘ 𝑊 ) ( Base ‘ 𝑊 ) ) )
15	14	simpld	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
16	14	simprd	⊢ ( 𝜑 → 𝑈 ( ⋖L ‘ 𝑊 ) ( Base ‘ 𝑊 ) )
17	11 1 2 4 12 5 15 7 8 9 16 10	l1cvat	⊢ ( 𝜑 → ( ( 𝑄 ⊕ 𝑅 ) ∩ 𝑈 ) ∈ 𝐴 )