Metamath Proof Explorer

Theorem doca2N

Description: Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses doca2.h 
|- H = ( LHyp ` K )
doca2.i 
|- I = ( ( DIsoA ` K ) ` W )
doca2.n 
|- ._|_ = ( ( ocA ` K ) ` W )
Assertion doca2N 
|- ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ._|_ ` ( ._|_ ` ( I ` X ) ) ) = ( I ` 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 hlol 
 |-  ( K e. HL -> K e. OL )
5 4 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> K e. OL )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 6 1 2 diadmclN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> X e. ( Base ` K ) )
8 6 1 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
9 8 ad2antlr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> W e. ( Base ` K ) )
10 eqid 
 |-  ( join ` K ) = ( join ` K )
11 eqid 
 |-  ( meet ` K ) = ( meet ` K )
12 eqid 
 |-  ( oc ` K ) = ( oc ` K )
13 6 10 11 12 oldmm1 
 |-  ( ( K e. OL /\ X e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( X ( meet ` K ) W ) ) = ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) )
14 5 7 9 13 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( oc ` K ) ` ( X ( meet ` K ) W ) ) = ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) )
15 14 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( oc ` K ) ` ( X ( meet ` K ) W ) ) ( meet ` K ) W ) = ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) )
16 15 eqcomd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) = ( ( ( oc ` K ) ` ( X ( meet ` K ) W ) ) ( meet ` K ) W ) )
17 16 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) = ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( X ( meet ` K ) W ) ) ( meet ` K ) W ) ) )
18 hllat 
 |-  ( K e. HL -> K e. Lat )
19 18 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> K e. Lat )
20 6 11 latmcl 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( X ( meet ` K ) W ) e. ( Base ` K ) )
21 19 7 9 20 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( X ( meet ` K ) W ) e. ( Base ` K ) )
22 6 10 11 12 oldmm2 
 |-  ( ( K e. OL /\ ( X ( meet ` K ) W ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( X ( meet ` K ) W ) ) ( meet ` K ) W ) ) = ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) )
23 5 21 9 22 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` ( X ( meet ` K ) W ) ) ( meet ` K ) W ) ) = ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) )
24 17 23 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) = ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) )
25 24 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) = ( ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) )
26 hlop 
 |-  ( K e. HL -> K e. OP )
27 26 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> K e. OP )
28 6 12 opoccl 
 |-  ( ( K e. OP /\ W e. ( Base ` K ) ) -> ( ( oc ` K ) ` W ) e. ( Base ` K ) )
29 27 9 28 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( oc ` K ) ` W ) e. ( Base ` K ) )
30 6 10 latjass 
 |-  ( ( K e. Lat /\ ( ( X ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) ) ) -> ( ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) = ( ( X ( meet ` K ) W ) ( join ` K ) ( ( ( oc ` K ) ` W ) ( join ` K ) ( ( oc ` K ) ` W ) ) ) )
31 19 21 29 29 30 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) = ( ( X ( meet ` K ) W ) ( join ` K ) ( ( ( oc ` K ) ` W ) ( join ` K ) ( ( oc ` K ) ` W ) ) ) )
32 6 10 latjidm 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) ) -> ( ( ( oc ` K ) ` W ) ( join ` K ) ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) )
33 19 29 32 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( oc ` K ) ` W ) ( join ` K ) ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) )
34 33 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( X ( meet ` K ) W ) ( join ` K ) ( ( ( oc ` K ) ` W ) ( join ` K ) ( ( oc ` K ) ` W ) ) ) = ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) )
35 31 34 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) = ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) )
36 25 35 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) = ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) )
37 36 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) = ( ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) )
38 hloml 
 |-  ( K e. HL -> K e. OML )
39 38 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> K e. OML )
40 eqid 
 |-  ( le ` K ) = ( le ` K )
41 6 40 11 latmle2 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( X ( meet ` K ) W ) ( le ` K ) W )
42 19 7 9 41 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( X ( meet ` K ) W ) ( le ` K ) W )
43 6 40 10 11 12 omlspjN 
 |-  ( ( K e. OML /\ ( ( X ( meet ` K ) W ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ ( X ( meet ` K ) W ) ( le ` K ) W ) -> ( ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) = ( X ( meet ` K ) W ) )
44 39 21 9 42 43 syl121anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( X ( meet ` K ) W ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) = ( X ( meet ` K ) W ) )
45 40 1 2 diadmleN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> X ( le ` K ) W )
46 6 40 11 latleeqm1 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( X ( le ` K ) W <-> ( X ( meet ` K ) W ) = X ) )
47 19 7 9 46 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( X ( le ` K ) W <-> ( X ( meet ` K ) W ) = X ) )
48 45 47 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( X ( meet ` K ) W ) = X )
49 37 44 48 3eqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> X = ( ( ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) )
50 49 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) = ( I ` ( ( ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) )
51 6 12 opoccl 
 |-  ( ( K e. OP /\ X e. ( Base ` K ) ) -> ( ( oc ` K ) ` X ) e. ( Base ` K ) )
52 27 7 51 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( oc ` K ) ` X ) e. ( Base ` K ) )
53 6 10 latjcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. ( Base ` K ) /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) e. ( Base ` K ) )
54 19 52 29 53 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) e. ( Base ` K ) )
55 6 11 latmcl 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) )
56 19 54 9 55 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) )
57 6 40 11 latmle2 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W )
58 19 54 9 57 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W )
59 6 40 1 2 diaeldm 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I <-> ( ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W ) ) )
60 59 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I <-> ( ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. ( Base ` K ) /\ ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ( le ` K ) W ) ) )
61 56 58 60 mpbir2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I )
62 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
63 10 11 12 1 62 2 3 diaocN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) e. dom I ) -> ( I ` ( ( ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) = ( ._|_ ` ( I ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) )
64 61 63 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` ( ( ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) = ( ._|_ ` ( I ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) )
65 10 11 12 1 62 2 3 diaocN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( I ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) = ( ._|_ ` ( I ` X ) ) )
66 65 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ._|_ ` ( I ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` W ) ) ( meet ` K ) W ) ) ) = ( ._|_ ` ( ._|_ ` ( I ` X ) ) ) )
67 50 64 66 3eqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. dom I ) -> ( ._|_ ` ( ._|_ ` ( I ` X ) ) ) = ( I ` X ) )