Metamath Proof Explorer


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