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 = ( LHyp ` K )
	dochexmidlem1.o	|- ._|_ = ( ( ocH ` K ) ` W )
	dochexmidlem1.u	|- U = ( ( DVecH ` K ) ` W )
	dochexmidlem1.v	|- V = ( Base ` U )
	dochexmidlem1.s	|- S = ( LSubSp ` U )
	dochexmidlem1.n	|- N = ( LSpan ` U )
	dochexmidlem1.p	|- .(+) = ( LSSum ` U )
	dochexmidlem1.a	|- A = ( LSAtoms ` U )
	dochexmidlem1.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dochexmidlem1.x	|- ( ph -> X e. S )
	dochexmidlem3.pp	|- ( ph -> p e. A )
	dochexmidlem3.qq	|- ( ph -> q e. A )
	dochexmidlem3.rr	|- ( ph -> r e. A )
	dochexmidlem3.ql	|- ( ph -> q C_ ( ._|_ ` X ) )
	dochexmidlem3.rl	|- ( ph -> r C_ X )
	dochexmidlem3.pl	|- ( ph -> q C_ ( r .(+) p ) )
Assertion	dochexmidlem3	|- ( ph -> p C_ ( X .(+) ( ._|_ ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		dochexmidlem1.h	|- H = ( LHyp ` K )
2		dochexmidlem1.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		dochexmidlem1.u	|- U = ( ( DVecH ` K ) ` W )
4		dochexmidlem1.v	|- V = ( Base ` U )
5		dochexmidlem1.s	|- S = ( LSubSp ` U )
6		dochexmidlem1.n	|- N = ( LSpan ` U )
7		dochexmidlem1.p	|- .(+) = ( LSSum ` U )
8		dochexmidlem1.a	|- A = ( LSAtoms ` U )
9		dochexmidlem1.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		dochexmidlem1.x	|- ( ph -> X e. S )
11		dochexmidlem3.pp	|- ( ph -> p e. A )
12		dochexmidlem3.qq	|- ( ph -> q e. A )
13		dochexmidlem3.rr	|- ( ph -> r e. A )
14		dochexmidlem3.ql	|- ( ph -> q C_ ( ._|_ ` X ) )
15		dochexmidlem3.rl	|- ( ph -> r C_ X )
16		dochexmidlem3.pl	|- ( ph -> q C_ ( r .(+) p ) )
17	1 3 9	dvhlvec	|- ( ph -> U e. LVec )
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	dochexmidlem1	|- ( ph -> q =/= r )
19	7 8 17 12 11 13 16 18	lsatexch1	|- ( ph -> p C_ ( r .(+) q ) )
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 19	dochexmidlem2	|- ( ph -> p C_ ( X .(+) ( ._|_ ` X ) ) )