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 = ( Base ` K )
	cmtcom.c	|- C = ( cm ` K )
Assertion	cmtcomN	|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> Y C X ) )

Proof

Step	Hyp	Ref	Expression
1		cmtcom.b	|- B = ( Base ` K )
2		cmtcom.c	|- C = ( cm ` K )
3	1 2	cmtcomlemN	|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y -> Y C X ) )
4	1 2	cmtcomlemN	|- ( ( K e. OML /\ Y e. B /\ X e. B ) -> ( Y C X -> X C Y ) )
5	4	3com23	|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( Y C X -> X C Y ) )
6	3 5	impbid	|- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X C Y <-> Y C X ) )