This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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