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	$$⊢B={\mathrm{Base}}_K$$
	cmtcom.c	$$⊢C=\mathrm{cm}\left(K\right)$$
Assertion	cmtcomN	$$⊢\left(K\in \mathrm{OML}\wedge X\in B\wedge Y\in B\right)\to \left(XCY\leftrightarrow YCX\right)$$

Proof

Step	Hyp	Ref	Expression
1		cmtcom.b	$$⊢B={\mathrm{Base}}_K$$
2		cmtcom.c	$$⊢C=\mathrm{cm}\left(K\right)$$
3	1 2	cmtcomlemN	$$⊢\left(K\in \mathrm{OML}\wedge X\in B\wedge Y\in B\right)\to \left(XCY\to YCX\right)$$
4	1 2	cmtcomlemN	$$⊢\left(K\in \mathrm{OML}\wedge Y\in B\wedge X\in B\right)\to \left(YCX\to XCY\right)$$
5	4	3com23	$$⊢\left(K\in \mathrm{OML}\wedge X\in B\wedge Y\in B\right)\to \left(YCX\to XCY\right)$$
6	3 5	impbid	$$⊢\left(K\in \mathrm{OML}\wedge X\in B\wedge Y\in B\right)\to \left(XCY\leftrightarrow YCX\right)$$