Theorem cmtcomN

Description: Commutation is symmetric. Theorem 2(v) in Kalmbach p. 22. ( cmcmi analog.) (Contributed by NM, 7-Nov-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cmtcom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cmtcom.c	⊢ 𝐶 = ( cm ‘ 𝐾 )
Assertion	cmtcomN	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑌 𝐶 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		cmtcom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cmtcom.c	⊢ 𝐶 = ( cm ‘ 𝐾 )
3	1 2	cmtcomlemN	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 → 𝑌 𝐶 𝑋 ) )
4	1 2	cmtcomlemN	⊢ ( ( 𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑋 → 𝑋 𝐶 𝑌 ) )
5	4	3com23	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑋 → 𝑋 𝐶 𝑌 ) )
6	3 5	impbid	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑌 𝐶 𝑋 ) )