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	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochexmidlem1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	dochexmidlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochexmidlem1.v	$$⊢V={\mathrm{Base}}_U$$
	dochexmidlem1.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
	dochexmidlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	dochexmidlem1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dochexmidlem1.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	dochexmidlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dochexmidlem1.x	$$⊢\phi \to X\in S$$
	dochexmidlem3.pp	$$⊢\phi \to p\in A$$
	dochexmidlem3.qq	$$⊢\phi \to q\in A$$
	dochexmidlem3.rr	$$⊢\phi \to r\in A$$
	dochexmidlem3.ql	$$⊢\phi \to q\subseteq \underset{\dot{}}{\perp }\left(X\right)$$
	dochexmidlem3.rl	$$⊢\phi \to r\subseteq X$$
	dochexmidlem3.pl	$$⊢\phi \to q\subseteq r\underset{\dot{}}{\oplus }p$$
Assertion	dochexmidlem3	$$⊢\phi \to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		dochexmidlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dochexmidlem1.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		dochexmidlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		dochexmidlem1.v	$$⊢V={\mathrm{Base}}_U$$
5		dochexmidlem1.s	$$⊢S=\mathrm{LSubSp}\left(U\right)$$
6		dochexmidlem1.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		dochexmidlem1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
8		dochexmidlem1.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
9		dochexmidlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		dochexmidlem1.x	$$⊢\phi \to X\in S$$
11		dochexmidlem3.pp	$$⊢\phi \to p\in A$$
12		dochexmidlem3.qq	$$⊢\phi \to q\in A$$
13		dochexmidlem3.rr	$$⊢\phi \to r\in A$$
14		dochexmidlem3.ql	$$⊢\phi \to q\subseteq \underset{\dot{}}{\perp }\left(X\right)$$
15		dochexmidlem3.rl	$$⊢\phi \to r\subseteq X$$
16		dochexmidlem3.pl	$$⊢\phi \to q\subseteq r\underset{\dot{}}{\oplus }p$$
17	1 3 9	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	dochexmidlem1	$$⊢\phi \to q\ne r$$
19	7 8 17 12 11 13 16 18	lsatexch1	$$⊢\phi \to p\subseteq r\underset{\dot{}}{\oplus }q$$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 19	dochexmidlem2	$$⊢\phi \to p\subseteq X\underset{\dot{}}{\oplus }\underset{\dot{}}{\perp }\left(X\right)$$