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 ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌𝑋 𝐶 ( 𝑌 ) ) )