Theorem dochexmidat

Description: Special case of excluded middle for the singleton of a vector. (Contributed by NM, 27-Oct-2014)

	Ref	Expression
Hypotheses	dochexmidat.h	|- H = ( LHyp ` K )
	dochexmidat.o	|- ._|_ = ( ( ocH ` K ) ` W )
	dochexmidat.u	|- U = ( ( DVecH ` K ) ` W )
	dochexmidat.v	|- V = ( Base ` U )
	dochexmidat.z	|- .0. = ( 0g ` U )
	dochexmidat.r	|- N = ( LSpan ` U )
	dochexmidat.p	|- .(+) = ( LSSum ` U )
	dochexmidat.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dochexmidat.x	|- ( ph -> X e. ( V \ { .0. } ) )
Assertion	dochexmidat	|- ( ph -> ( ( ._|_ ` { X } ) .(+) ( N ` { X } ) ) = V )

Proof

Step	Hyp	Ref	Expression
1		dochexmidat.h	|- H = ( LHyp ` K )
2		dochexmidat.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		dochexmidat.u	|- U = ( ( DVecH ` K ) ` W )
4		dochexmidat.v	|- V = ( Base ` U )
5		dochexmidat.z	|- .0. = ( 0g ` U )
6		dochexmidat.r	|- N = ( LSpan ` U )
7		dochexmidat.p	|- .(+) = ( LSSum ` U )
8		dochexmidat.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		dochexmidat.x	|- ( ph -> X e. ( V \ { .0. } ) )
10	1 2 3 4 5 8 9	dochnel	|- ( ph -> -. X e. ( ._|_ ` { X } ) )
11		eqid	|- ( LSHyp ` U ) = ( LSHyp ` U )
12	1 3 8	dvhlvec	|- ( ph -> U e. LVec )
13	1 2 3 4 5 11 8 9	dochsnshp	|- ( ph -> ( ._|_ ` { X } ) e. ( LSHyp ` U ) )
14	9	eldifad	|- ( ph -> X e. V )
15	4 6 7 11 12 13 14	lshpnelb	|- ( ph -> ( -. X e. ( ._|_ ` { X } ) <-> ( ( ._|_ ` { X } ) .(+) ( N ` { X } ) ) = V ) )
16	10 15	mpbid	|- ( ph -> ( ( ._|_ ` { X } ) .(+) ( N ` { X } ) ) = V )