Theorem doca3N

Description: Double orthocomplement of partial isomorphism A. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	doca2.h	|- H = ( LHyp ` K )
	doca2.i	|- I = ( ( DIsoA ` K ) ` W )
	doca2.n	|- ._|_ = ( ( ocA ` K ) ` W )
Assertion	doca3N	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )

Proof

Step	Hyp	Ref	Expression
1		doca2.h	|- H = ( LHyp ` K )
2		doca2.i	|- I = ( ( DIsoA ` K ) ` W )
3		doca2.n	|- ._|_ = ( ( ocA ` K ) ` W )
4	1 2	diacnvclN	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. dom I )
5	1 2 3	doca2N	|- ( ( ( K e. HL /\ W e. H ) /\ ( `' I ` X ) e. dom I ) -> ( ._|_ ` ( ._|_ ` ( I ` ( `' I ` X ) ) ) ) = ( I ` ( `' I ` X ) ) )
6	4 5	syldan	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( ._|_ ` ( I ` ( `' I ` X ) ) ) ) = ( I ` ( `' I ` X ) ) )
7	1 2	diaf11N	|- ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )
8		f1ocnvfv2	|- ( ( I : dom I -1-1-onto-> ran I /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X )
9	7 8	sylan	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X )
10	9	fveq2d	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( I ` ( `' I ` X ) ) ) = ( ._|_ ` X ) )
11	10	fveq2d	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( ._|_ ` ( I ` ( `' I ` X ) ) ) ) = ( ._|_ ` ( ._|_ ` X ) ) )
12	6 11 9	3eqtr3d	|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )