This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )