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 ⊢ Base K = Base K
7 6 1 2 diadmclN ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → X ∈ Base K
8 6 1 lhpbase ⊢ W ∈ H → W ∈ Base K
9 8 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → W ∈ 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 ∈ OL ∧ X ∈ Base K ∧ W ∈ Base K → oc ⁡ K ⁡ X meet ⁡ K W = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W
14 5 7 9 13 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → oc ⁡ K ⁡ X meet ⁡ K W = oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W
15 14 oveq1d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ HL → K ∈ Lat
19 18 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → K ∈ Lat
20 6 11 latmcl ⊢ K ∈ Lat ∧ X ∈ Base K ∧ W ∈ Base K → X meet ⁡ K W ∈ Base K
21 19 7 9 20 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → X meet ⁡ K W ∈ Base K
22 6 10 11 12 oldmm2 ⊢ K ∈ OL ∧ X meet ⁡ K W ∈ Base K ∧ W ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ HL → K ∈ OP
27 26 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → K ∈ OP
28 6 12 opoccl ⊢ K ∈ OP ∧ W ∈ Base K → oc ⁡ K ⁡ W ∈ Base K
29 27 9 28 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → oc ⁡ K ⁡ W ∈ Base K
30 6 10 latjass ⊢ K ∈ Lat ∧ X meet ⁡ K W ∈ Base K ∧ oc ⁡ K ⁡ W ∈ Base K ∧ oc ⁡ K ⁡ W ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ Lat ∧ oc ⁡ K ⁡ W ∈ Base K → oc ⁡ K ⁡ W join ⁡ K oc ⁡ K ⁡ W = oc ⁡ K ⁡ W
33 19 29 32 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → oc ⁡ K ⁡ W join ⁡ K oc ⁡ K ⁡ W = oc ⁡ K ⁡ W
34 33 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ 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 ∈ Base K ∧ W ∈ Base K → X meet ⁡ K W ≤ K W
42 19 7 9 41 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → X meet ⁡ K W ≤ K W
43 6 40 10 11 12 omlspjN ⊢ K ∈ OML ∧ X meet ⁡ K W ∈ Base K ∧ W ∈ Base K ∧ X meet ⁡ K W ≤ 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 ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → X meet ⁡ K W join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W = X meet ⁡ K W
45 40 1 2 diadmleN ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → X ≤ K W
46 6 40 11 latleeqm1 ⊢ K ∈ Lat ∧ X ∈ Base K ∧ W ∈ Base K → X ≤ K W ↔ X meet ⁡ K W = X
47 19 7 9 46 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → X ≤ K W ↔ X meet ⁡ K W = X
48 45 47 mpbid ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → X meet ⁡ K W = X
49 37 44 48 3eqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ OP ∧ X ∈ Base K → oc ⁡ K ⁡ X ∈ Base K
52 27 7 51 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → oc ⁡ K ⁡ X ∈ Base K
53 6 10 latjcl ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ X ∈ Base K ∧ oc ⁡ K ⁡ W ∈ Base K → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W ∈ Base K
54 19 52 29 53 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W ∈ Base K
55 6 11 latmcl ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W ∈ Base K ∧ W ∈ Base K → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ Base K
56 19 54 9 55 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ Base K
57 6 40 11 latmle2 ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W ∈ Base K ∧ W ∈ Base K → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ≤ K W
58 19 54 9 57 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ≤ K W
59 6 40 1 2 diaeldm ⊢ K ∈ HL ∧ W ∈ H → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ dom ⁡ I ↔ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ Base K ∧ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ≤ K W
60 59 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ dom ⁡ I ↔ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ Base K ∧ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ≤ K W
61 56 58 60 mpbir2and ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ 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 ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ 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 ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → I ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W = ⊥ ˙ ⁡ I ⁡ X
66 65 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → ⊥ ˙ ⁡ I ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ W meet ⁡ K W = ⊥ ˙ ⁡ ⊥ ˙ ⁡ I ⁡ X
67 50 64 66 3eqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ dom ⁡ I → ⊥ ˙ ⁡ ⊥ ˙ ⁡ I ⁡ X = I ⁡ X