Metamath Proof Explorer


Theorem cmt3N

Description: Commutation with orthocomplement. Remark in Kalmbach p. 23. ( cmcm4i analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cmt2.b 𝐵 = ( Base ‘ 𝐾 )
cmt2.o = ( oc ‘ 𝐾 )
cmt2.c 𝐶 = ( cm ‘ 𝐾 )
Assertion cmt3N ( ( 𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ) 𝐶 𝑌 ) )

Proof

Step Hyp Ref Expression
1 cmt2.b 𝐵 = ( Base ‘ 𝐾 )
2 cmt2.o = ( oc ‘ 𝐾 )
3 cmt2.c 𝐶 = ( cm ‘ 𝐾 )
4 1 2 3 cmt2N ( ( 𝐾 ∈ OML ∧ 𝑌𝐵𝑋𝐵 ) → ( 𝑌 𝐶 𝑋𝑌 𝐶 ( 𝑋 ) ) )
5 4 3com23 ( ( 𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑌 𝐶 𝑋𝑌 𝐶 ( 𝑋 ) ) )
6 1 3 cmtcomN ( ( 𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌𝑌 𝐶 𝑋 ) )
7 omlop ( 𝐾 ∈ OML → 𝐾 ∈ OP )
8 7 3ad2ant1 ( ( 𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵 ) → 𝐾 ∈ OP )
9 simp2 ( ( 𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵 ) → 𝑋𝐵 )
10 1 2 opoccl ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → ( 𝑋 ) ∈ 𝐵 )
11 8 9 10 syl2anc ( ( 𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 ) ∈ 𝐵 )
12 1 3 cmtcomN ( ( 𝐾 ∈ OML ∧ ( 𝑋 ) ∈ 𝐵𝑌𝐵 ) → ( ( 𝑋 ) 𝐶 𝑌𝑌 𝐶 ( 𝑋 ) ) )
13 11 12 syld3an2 ( ( 𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵 ) → ( ( 𝑋 ) 𝐶 𝑌𝑌 𝐶 ( 𝑋 ) ) )
14 5 6 13 3bitr4d ( ( 𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 ) 𝐶 𝑌 ) )