Metamath Proof Explorer

Theorem cmt2N

Description: Commutation with orthocomplement. Theorem 2.3(i) of Beran p. 39. ( cmcm2i analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cmt2.b ⊢ B = Base K
cmt2.o ⊢ ⊥ ˙ = oc ⁡ K
cmt2.c ⊢ C = cm ⁡ K
Assertion cmt2N ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X C Y ↔ X C ⊥ ˙ ⁡ Y

Proof

Step Hyp Ref Expression
1 cmt2.b ⊢ B = Base K
2 cmt2.o ⊢ ⊥ ˙ = oc ⁡ K
3 cmt2.c ⊢ C = cm ⁡ K
4 omllat ⊢ K ∈ OML → K ∈ Lat
5 4 3ad2ant1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → K ∈ Lat
6 eqid ⊢ meet ⁡ K = meet ⁡ K
7 1 6 latmcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y ∈ B
8 4 7 syl3an1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y ∈ B
9 simp2 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X ∈ B
10 omlop ⊢ K ∈ OML → K ∈ OP
11 10 3ad2ant1 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → K ∈ OP
12 simp3 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
13 1 2 opoccl ⊢ K ∈ OP ∧ Y ∈ B → ⊥ ˙ ⁡ Y ∈ B
14 11 12 13 syl2anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ Y ∈ B
15 1 6 latmcl ⊢ K ∈ Lat ∧ X ∈ B ∧ ⊥ ˙ ⁡ Y ∈ B → X meet ⁡ K ⊥ ˙ ⁡ Y ∈ B
16 5 9 14 15 syl3anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K ⊥ ˙ ⁡ Y ∈ B
17 eqid ⊢ join ⁡ K = join ⁡ K
18 1 17 latjcom ⊢ K ∈ Lat ∧ X meet ⁡ K Y ∈ B ∧ X meet ⁡ K ⊥ ˙ ⁡ Y ∈ B → X meet ⁡ K Y join ⁡ K X meet ⁡ K ⊥ ˙ ⁡ Y = X meet ⁡ K ⊥ ˙ ⁡ Y join ⁡ K X meet ⁡ K Y
19 5 8 16 18 syl3anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y join ⁡ K X meet ⁡ K ⊥ ˙ ⁡ Y = X meet ⁡ K ⊥ ˙ ⁡ Y join ⁡ K X meet ⁡ K Y
20 1 2 opococ ⊢ K ∈ OP ∧ Y ∈ B → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y
21 11 12 20 syl2anc ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y
22 21 oveq2d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = X meet ⁡ K Y
23 22 oveq2d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K ⊥ ˙ ⁡ Y join ⁡ K X meet ⁡ K ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = X meet ⁡ K ⊥ ˙ ⁡ Y join ⁡ K X meet ⁡ K Y
24 19 23 eqtr4d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X meet ⁡ K Y join ⁡ K X meet ⁡ K ⊥ ˙ ⁡ Y = X meet ⁡ K ⊥ ˙ ⁡ Y join ⁡ K X meet ⁡ K ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y
25 24 eqeq2d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X = X meet ⁡ K Y join ⁡ K X meet ⁡ K ⊥ ˙ ⁡ Y ↔ X = X meet ⁡ K ⊥ ˙ ⁡ Y join ⁡ K X meet ⁡ K ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y
26 1 17 6 2 3 cmtvalN ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X C Y ↔ X = X meet ⁡ K Y join ⁡ K X meet ⁡ K ⊥ ˙ ⁡ Y
27 1 17 6 2 3 cmtvalN ⊢ K ∈ OML ∧ X ∈ B ∧ ⊥ ˙ ⁡ Y ∈ B → X C ⊥ ˙ ⁡ Y ↔ X = X meet ⁡ K ⊥ ˙ ⁡ Y join ⁡ K X meet ⁡ K ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y
28 14 27 syld3an3 ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X C ⊥ ˙ ⁡ Y ↔ X = X meet ⁡ K ⊥ ˙ ⁡ Y join ⁡ K X meet ⁡ K ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y
29 25 26 28 3bitr4d ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B → X C Y ↔ X C ⊥ ˙ ⁡ Y