Theorem dochocsn

Description: The double orthocomplement of a singleton is its span. (Contributed by NM, 13-Jan-2015)

	Ref	Expression
Hypotheses	dochocsn.h	|- H = ( LHyp ` K )
	dochocsn.u	|- U = ( ( DVecH ` K ) ` W )
	dochocsn.o	|- ._|_ = ( ( ocH ` K ) ` W )
	dochocsn.v	|- V = ( Base ` U )
	dochocsn.n	|- N = ( LSpan ` U )
	dochocsn.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	dochocsn.x	|- ( ph -> X e. V )
Assertion	dochocsn	|- ( ph -> ( ._|_ ` ( ._|_ ` { X } ) ) = ( N ` { X } ) )

Proof

Step	Hyp	Ref	Expression
1		dochocsn.h	|- H = ( LHyp ` K )
2		dochocsn.u	|- U = ( ( DVecH ` K ) ` W )
3		dochocsn.o	|- ._|_ = ( ( ocH ` K ) ` W )
4		dochocsn.v	|- V = ( Base ` U )
5		dochocsn.n	|- N = ( LSpan ` U )
6		dochocsn.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		dochocsn.x	|- ( ph -> X e. V )
8	7	snssd	|- ( ph -> { X } C_ V )
9	1 2 3 4 5 6 8	dochocsp	|- ( ph -> ( ._|_ ` ( N ` { X } ) ) = ( ._|_ ` { X } ) )
10	9	fveq2d	|- ( ph -> ( ._|_ ` ( ._|_ ` ( N ` { X } ) ) ) = ( ._|_ ` ( ._|_ ` { X } ) ) )
11		eqid	|- ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
12	1 2 4 5 11	dihlsprn	|- ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
13	6 7 12	syl2anc	|- ( ph -> ( N ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
14	1 11 3	dochoc	|- ( ( ( K e. HL /\ W e. H ) /\ ( N ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( N ` { X } ) ) ) = ( N ` { X } ) )
15	6 13 14	syl2anc	|- ( ph -> ( ._|_ ` ( ._|_ ` ( N ` { X } ) ) ) = ( N ` { X } ) )
16	10 15	eqtr3d	|- ( ph -> ( ._|_ ` ( ._|_ ` { X } ) ) = ( N ` { X } ) )