Theorem dochvalr2

Description: Orthocomplement of a closed subspace. (Contributed by NM, 21-Jul-2014)

	Ref	Expression
Hypotheses	dochvalr2.b	|- B = ( Base ` K )
	dochvalr2.o	|- ._|_ = ( oc ` K )
	dochvalr2.h	|- H = ( LHyp ` K )
	dochvalr2.i	|- I = ( ( DIsoH ` K ) ` W )
	dochvalr2.n	|- N = ( ( ocH ` K ) ` W )
Assertion	dochvalr2	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( N ` ( I ` X ) ) = ( I ` ( ._|_ ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		dochvalr2.b	|- B = ( Base ` K )
2		dochvalr2.o	|- ._|_ = ( oc ` K )
3		dochvalr2.h	|- H = ( LHyp ` K )
4		dochvalr2.i	|- I = ( ( DIsoH ` K ) ` W )
5		dochvalr2.n	|- N = ( ( ocH ` K ) ` W )
6	1 3 4	dihcl	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` X ) e. ran I )
7	2 3 4 5	dochvalr	|- ( ( ( K e. HL /\ W e. H ) /\ ( I ` X ) e. ran I ) -> ( N ` ( I ` X ) ) = ( I ` ( ._|_ ` ( `' I ` ( I ` X ) ) ) ) )
8	6 7	syldan	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( N ` ( I ` X ) ) = ( I ` ( ._|_ ` ( `' I ` ( I ` X ) ) ) ) )
9	1 3 4	dihcnvid1	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( `' I ` ( I ` X ) ) = X )
10	9	fveq2d	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( ._|_ ` ( `' I ` ( I ` X ) ) ) = ( ._|_ ` X ) )
11	10	fveq2d	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( I ` ( ._|_ ` ( `' I ` ( I ` X ) ) ) ) = ( I ` ( ._|_ ` X ) ) )
12	8 11	eqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ X e. B ) -> ( N ` ( I ` X ) ) = ( I ` ( ._|_ ` X ) ) )