Metamath Proof Explorer

Theorem diaocN

Description: Value of partial isomorphism A at lattice orthocomplement (using a Sasaki projection to get orthocomplement relative to the fiducial co-atom W ). (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses diaoc.j 
|- .\/ = ( join ` K )
diaoc.m 
|- ./\ = ( meet ` K )
diaoc.o 
|- ._|_ = ( oc ` K )
diaoc.h 
|- H = ( LHyp ` K )
diaoc.t 
|- T = ( ( LTrn ` K ) ` W )
diaoc.i 
|- I = ( ( DIsoA ` K ) ` W )
diaoc.n 
|- N = ( ( ocA ` K ) ` W )
Assertion diaocN 
|- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` ( ( ( ._|_ ` X ) .\/ ( ._|_ ` W ) ) ./\ W ) ) = ( N ` ( I ` X ) ) )

Proof

Step Hyp Ref Expression
1 diaoc.j 
 |-  .\/ = ( join ` K )
2 diaoc.m 
 |-  ./\ = ( meet ` K )
3 diaoc.o 
 |-  ._|_ = ( oc ` K )
4 diaoc.h 
 |-  H = ( LHyp ` K )
5 diaoc.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 diaoc.i 
 |-  I = ( ( DIsoA ` K ) ` W )
7 diaoc.n 
 |-  N = ( ( ocA ` K ) ` W )
8 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( K e. HL /\ W e. H ) )
9 eqid 
 |-  ( Base ` K ) = ( Base ` K )
10 9 4 6 diadmclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> X e. ( Base ` K ) )
11 eqid 
 |-  ( le ` K ) = ( le ` K )
12 11 4 6 diadmleN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> X ( le ` K ) W )
13 9 11 4 5 6 diass 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. ( Base ` K ) /\ X ( le ` K ) W ) ) -> ( I ` X ) C_ T )
14 8 10 12 13 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) C_ T )
15 1 2 3 4 5 6 7 docavalN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( I ` X ) C_ T ) -> ( N ` ( I ` X ) ) = ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | ( I ` X ) C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )
16 14 15 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( N ` ( I ` X ) ) = ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | ( I ` X ) C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )
17 4 6 diaclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) e. ran I )
18 intmin 
 |-  ( ( I ` X ) e. ran I -> |^| { z e. ran I | ( I ` X ) C_ z } = ( I ` X ) )
19 17 18 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> |^| { z e. ran I | ( I ` X ) C_ z } = ( I ` X ) )
20 19 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( `' I ` |^| { z e. ran I | ( I ` X ) C_ z } ) = ( `' I ` ( I ` X ) ) )
21 4 6 diaf11N 
 |-  ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )
22 f1ocnvfv1 
 |-  ( ( I : dom I -1-1-onto-> ran I /\ X e. dom I ) -> ( `' I ` ( I ` X ) ) = X )
23 21 22 sylan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( `' I ` ( I ` X ) ) = X )
24 20 23 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( `' I ` |^| { z e. ran I | ( I ` X ) C_ z } ) = X )
25 24 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ._|_ ` ( `' I ` |^| { z e. ran I | ( I ` X ) C_ z } ) ) = ( ._|_ ` X ) )
26 25 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ._|_ ` ( `' I ` |^| { z e. ran I | ( I ` X ) C_ z } ) ) .\/ ( ._|_ ` W ) ) = ( ( ._|_ ` X ) .\/ ( ._|_ ` W ) ) )
27 26 fvoveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` ( ( ( ._|_ ` ( `' I ` |^| { z e. ran I | ( I ` X ) C_ z } ) ) .\/ ( ._|_ ` W ) ) ./\ W ) ) = ( I ` ( ( ( ._|_ ` X ) .\/ ( ._|_ ` W ) ) ./\ W ) ) )
28 16 27 eqtr2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` ( ( ( ._|_ ` X ) .\/ ( ._|_ ` W ) ) ./\ W ) ) = ( N ` ( I ` X ) ) )