Theorem dochexmidlem3

Description: Lemma for dochexmid . Use atom exchange lsatexch1 to swap p and q . (Contributed by NM, 14-Jan-2015)

	Ref	Expression
Hypotheses	dochexmidlem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochexmidlem1.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochexmidlem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochexmidlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochexmidlem1.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
	dochexmidlem1.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	dochexmidlem1.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
	dochexmidlem1.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
	dochexmidlem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochexmidlem1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	dochexmidlem3.pp	⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
	dochexmidlem3.qq	⊢ ( 𝜑 → 𝑞 ∈ 𝐴 )
	dochexmidlem3.rr	⊢ ( 𝜑 → 𝑟 ∈ 𝐴 )
	dochexmidlem3.ql	⊢ ( 𝜑 → 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) )
	dochexmidlem3.rl	⊢ ( 𝜑 → 𝑟 ⊆ 𝑋 )
	dochexmidlem3.pl	⊢ ( 𝜑 → 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) )
Assertion	dochexmidlem3	⊢ ( 𝜑 → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dochexmidlem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochexmidlem1.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochexmidlem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochexmidlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochexmidlem1.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
6		dochexmidlem1.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
7		dochexmidlem1.p	⊢ ⊕ = ( LSSum ‘ 𝑈 )
8		dochexmidlem1.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
9		dochexmidlem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		dochexmidlem1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
11		dochexmidlem3.pp	⊢ ( 𝜑 → 𝑝 ∈ 𝐴 )
12		dochexmidlem3.qq	⊢ ( 𝜑 → 𝑞 ∈ 𝐴 )
13		dochexmidlem3.rr	⊢ ( 𝜑 → 𝑟 ∈ 𝐴 )
14		dochexmidlem3.ql	⊢ ( 𝜑 → 𝑞 ⊆ ( ⊥ ‘ 𝑋 ) )
15		dochexmidlem3.rl	⊢ ( 𝜑 → 𝑟 ⊆ 𝑋 )
16		dochexmidlem3.pl	⊢ ( 𝜑 → 𝑞 ⊆ ( 𝑟 ⊕ 𝑝 ) )
17	1 3 9	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	dochexmidlem1	⊢ ( 𝜑 → 𝑞 ≠ 𝑟 )
19	7 8 17 12 11 13 16 18	lsatexch1	⊢ ( 𝜑 → 𝑝 ⊆ ( 𝑟 ⊕ 𝑞 ) )
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 19	dochexmidlem2	⊢ ( 𝜑 → 𝑝 ⊆ ( 𝑋 ⊕ ( ⊥ ‘ 𝑋 ) ) )