Theorem dochspocN

Description: The span of an orthocomplement equals the orthocomplement of the span. (Contributed by NM, 7-Aug-2014) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dochsp.h	|- H = ( LHyp ` K )
2		dochsp.u	|- U = ( ( DVecH ` K ) ` W )
3		dochsp.o	|- ._|_ = ( ( ocH ` K ) ` W )
4		dochsp.v	|- V = ( Base ` U )
5		dochsp.n	|- N = ( LSpan ` U )
6		dochsp.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		dochsp.x	|- ( ph -> X C_ V )
8	1 2 6	dvhlmod	|- ( ph -> U e. LMod )
9		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
10	1 2 4 9 3	dochlss	|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) e. ( LSubSp ` U ) )
11	6 7 10	syl2anc	|- ( ph -> ( ._|_ ` X ) e. ( LSubSp ` U ) )
12	9 5	lspid	|- ( ( U e. LMod /\ ( ._|_ ` X ) e. ( LSubSp ` U ) ) -> ( N ` ( ._|_ ` X ) ) = ( ._|_ ` X ) )
13	8 11 12	syl2anc	|- ( ph -> ( N ` ( ._|_ ` X ) ) = ( ._|_ ` X ) )
14	1 2 3 4 5 6 7	dochocsp	|- ( ph -> ( ._|_ ` ( N ` X ) ) = ( ._|_ ` X ) )
15	13 14	eqtr4d	|- ( ph -> ( N ` ( ._|_ ` X ) ) = ( ._|_ ` ( N ` X ) ) )