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

Metamath Proof Explorer

Theorem cmt4N

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	cmt4N	⊢ ( ( 𝐾 ∈ 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		omlop	⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP )
6	5	3ad2ant1	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP )
7		simp3	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
8	1 2	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
9	6 7 8	syl2anc	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
10	1 2 3	cmt3N	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 𝐶 ( ⊥ ‘ 𝑌 ) ↔ ( ⊥ ‘ 𝑋 ) 𝐶 ( ⊥ ‘ 𝑌 ) ) )
11	9 10	syld3an3	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 ( ⊥ ‘ 𝑌 ) ↔ ( ⊥ ‘ 𝑋 ) 𝐶 ( ⊥ ‘ 𝑌 ) ) )
12	4 11	bitrd	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( ⊥ ‘ 𝑋 ) 𝐶 ( ⊥ ‘ 𝑌 ) ) )