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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
cmt2.o ⊢ ⊥ = ( oc ‘ 𝐾 )
cmt2.c ⊢ 𝐶 = ( cm ‘ 𝐾 )
Assertion cmt2N ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑋 𝐶 ( ⊥ ‘ 𝑌 ) ) )

Proof

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