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∈HL∧W∈H∧X∈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∈HL→K∈OL
5 4 ad2antrr ⊢K∈HL∧W∈H∧X∈dom⁡I→K∈OL
6 eqid ⊢BaseK=BaseK
7 6 1 2 diadmclN ⊢K∈HL∧W∈H∧X∈dom⁡I→X∈BaseK
8 6 1 lhpbase ⊢W∈H→W∈BaseK
9 8 ad2antlr ⊢K∈HL∧W∈H∧X∈dom⁡I→W∈BaseK
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∈OL∧X∈BaseK∧W∈BaseK→oc⁡K⁡Xmeet⁡KW=oc⁡K⁡Xjoin⁡Koc⁡K⁡W
14 5 7 9 13 syl3anc ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡Xmeet⁡KW=oc⁡K⁡Xjoin⁡Koc⁡K⁡W
15 14 oveq1d ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡Xmeet⁡KWmeet⁡KW=oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW
16 15 eqcomd ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW=oc⁡K⁡Xmeet⁡KWmeet⁡KW
17 16 fveq2d ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW=oc⁡K⁡oc⁡K⁡Xmeet⁡KWmeet⁡KW
18 hllat ⊢K∈HL→K∈Lat
19 18 ad2antrr ⊢K∈HL∧W∈H∧X∈dom⁡I→K∈Lat
20 6 11 latmcl ⊢K∈Lat∧X∈BaseK∧W∈BaseK→Xmeet⁡KW∈BaseK
21 19 7 9 20 syl3anc ⊢K∈HL∧W∈H∧X∈dom⁡I→Xmeet⁡KW∈BaseK
22 6 10 11 12 oldmm2 ⊢K∈OL∧Xmeet⁡KW∈BaseK∧W∈BaseK→oc⁡K⁡oc⁡K⁡Xmeet⁡KWmeet⁡KW=Xmeet⁡KWjoin⁡Koc⁡K⁡W
23 5 21 9 22 syl3anc ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡oc⁡K⁡Xmeet⁡KWmeet⁡KW=Xmeet⁡KWjoin⁡Koc⁡K⁡W
24 17 23 eqtrd ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW=Xmeet⁡KWjoin⁡Koc⁡K⁡W
25 24 oveq1d ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KWjoin⁡Koc⁡K⁡W=Xmeet⁡KWjoin⁡Koc⁡K⁡Wjoin⁡Koc⁡K⁡W
26 hlop ⊢K∈HL→K∈OP
27 26 ad2antrr ⊢K∈HL∧W∈H∧X∈dom⁡I→K∈OP
28 6 12 opoccl ⊢K∈OP∧W∈BaseK→oc⁡K⁡W∈BaseK
29 27 9 28 syl2anc ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡W∈BaseK
30 6 10 latjass ⊢K∈Lat∧Xmeet⁡KW∈BaseK∧oc⁡K⁡W∈BaseK∧oc⁡K⁡W∈BaseK→Xmeet⁡KWjoin⁡Koc⁡K⁡Wjoin⁡Koc⁡K⁡W=Xmeet⁡KWjoin⁡Koc⁡K⁡Wjoin⁡Koc⁡K⁡W
31 19 21 29 29 30 syl13anc ⊢K∈HL∧W∈H∧X∈dom⁡I→Xmeet⁡KWjoin⁡Koc⁡K⁡Wjoin⁡Koc⁡K⁡W=Xmeet⁡KWjoin⁡Koc⁡K⁡Wjoin⁡Koc⁡K⁡W
32 6 10 latjidm ⊢K∈Lat∧oc⁡K⁡W∈BaseK→oc⁡K⁡Wjoin⁡Koc⁡K⁡W=oc⁡K⁡W
33 19 29 32 syl2anc ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡Wjoin⁡Koc⁡K⁡W=oc⁡K⁡W
34 33 oveq2d ⊢K∈HL∧W∈H∧X∈dom⁡I→Xmeet⁡KWjoin⁡Koc⁡K⁡Wjoin⁡Koc⁡K⁡W=Xmeet⁡KWjoin⁡Koc⁡K⁡W
35 31 34 eqtrd ⊢K∈HL∧W∈H∧X∈dom⁡I→Xmeet⁡KWjoin⁡Koc⁡K⁡Wjoin⁡Koc⁡K⁡W=Xmeet⁡KWjoin⁡Koc⁡K⁡W
36 25 35 eqtrd ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KWjoin⁡Koc⁡K⁡W=Xmeet⁡KWjoin⁡Koc⁡K⁡W
37 36 oveq1d ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KWjoin⁡Koc⁡K⁡Wmeet⁡KW=Xmeet⁡KWjoin⁡Koc⁡K⁡Wmeet⁡KW
38 hloml ⊢K∈HL→K∈OML
39 38 ad2antrr ⊢K∈HL∧W∈H∧X∈dom⁡I→K∈OML
40 eqid ⊢≤K=≤K
41 6 40 11 latmle2 ⊢K∈Lat∧X∈BaseK∧W∈BaseK→Xmeet⁡KW≤KW
42 19 7 9 41 syl3anc ⊢K∈HL∧W∈H∧X∈dom⁡I→Xmeet⁡KW≤KW
43 6 40 10 11 12 omlspjN ⊢K∈OML∧Xmeet⁡KW∈BaseK∧W∈BaseK∧Xmeet⁡KW≤KW→Xmeet⁡KWjoin⁡Koc⁡K⁡Wmeet⁡KW=Xmeet⁡KW
44 39 21 9 42 43 syl121anc ⊢K∈HL∧W∈H∧X∈dom⁡I→Xmeet⁡KWjoin⁡Koc⁡K⁡Wmeet⁡KW=Xmeet⁡KW
45 40 1 2 diadmleN ⊢K∈HL∧W∈H∧X∈dom⁡I→X≤KW
46 6 40 11 latleeqm1 ⊢K∈Lat∧X∈BaseK∧W∈BaseK→X≤KW↔Xmeet⁡KW=X
47 19 7 9 46 syl3anc ⊢K∈HL∧W∈H∧X∈dom⁡I→X≤KW↔Xmeet⁡KW=X
48 45 47 mpbid ⊢K∈HL∧W∈H∧X∈dom⁡I→Xmeet⁡KW=X
49 37 44 48 3eqtrrd ⊢K∈HL∧W∈H∧X∈dom⁡I→X=oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KWjoin⁡Koc⁡K⁡Wmeet⁡KW
50 49 fveq2d ⊢K∈HL∧W∈H∧X∈dom⁡I→I⁡X=I⁡oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KWjoin⁡Koc⁡K⁡Wmeet⁡KW
51 6 12 opoccl ⊢K∈OP∧X∈BaseK→oc⁡K⁡X∈BaseK
52 27 7 51 syl2anc ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡X∈BaseK
53 6 10 latjcl ⊢K∈Lat∧oc⁡K⁡X∈BaseK∧oc⁡K⁡W∈BaseK→oc⁡K⁡Xjoin⁡Koc⁡K⁡W∈BaseK
54 19 52 29 53 syl3anc ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡Xjoin⁡Koc⁡K⁡W∈BaseK
55 6 11 latmcl ⊢K∈Lat∧oc⁡K⁡Xjoin⁡Koc⁡K⁡W∈BaseK∧W∈BaseK→oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW∈BaseK
56 19 54 9 55 syl3anc ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW∈BaseK
57 6 40 11 latmle2 ⊢K∈Lat∧oc⁡K⁡Xjoin⁡Koc⁡K⁡W∈BaseK∧W∈BaseK→oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW≤KW
58 19 54 9 57 syl3anc ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW≤KW
59 6 40 1 2 diaeldm ⊢K∈HL∧W∈H→oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW∈dom⁡I↔oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW∈BaseK∧oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW≤KW
60 59 adantr ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW∈dom⁡I↔oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW∈BaseK∧oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW≤KW
61 56 58 60 mpbir2and ⊢K∈HL∧W∈H∧X∈dom⁡I→oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW∈dom⁡I
62 eqid ⊢LTrn⁡K⁡W=LTrn⁡K⁡W
63 10 11 12 1 62 2 3 diaocN ⊢K∈HL∧W∈H∧oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW∈dom⁡I→I⁡oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KWjoin⁡Koc⁡K⁡Wmeet⁡KW=⊥˙⁡I⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW
64 61 63 syldan ⊢K∈HL∧W∈H∧X∈dom⁡I→I⁡oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KWjoin⁡Koc⁡K⁡Wmeet⁡KW=⊥˙⁡I⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW
65 10 11 12 1 62 2 3 diaocN ⊢K∈HL∧W∈H∧X∈dom⁡I→I⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW=⊥˙⁡I⁡X
66 65 fveq2d ⊢K∈HL∧W∈H∧X∈dom⁡I→⊥˙⁡I⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Wmeet⁡KW=⊥˙⁡⊥˙⁡I⁡X
67 50 64 66 3eqtrrd ⊢K∈HL∧W∈H∧X∈dom⁡I→⊥˙⁡⊥˙⁡I⁡X=I⁡X