Theorem crngocom

Description: The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010)

	Ref	Expression
Hypotheses	crngocom.1	|- G = ( 1st ` R )
	crngocom.2	|- H = ( 2nd ` R )
	crngocom.3	|- X = ran G
Assertion	crngocom	|- ( ( R e. CRingOps /\ A e. X /\ B e. X ) -> ( A H B ) = ( B H A ) )

Proof

Step	Hyp	Ref	Expression
1		crngocom.1	|- G = ( 1st ` R )
2		crngocom.2	|- H = ( 2nd ` R )
3		crngocom.3	|- X = ran G
4	1 2 3	iscrngo2	|- ( R e. CRingOps <-> ( R e. RingOps /\ A. x e. X A. y e. X ( x H y ) = ( y H x ) ) )
5	4	simprbi	|- ( R e. CRingOps -> A. x e. X A. y e. X ( x H y ) = ( y H x ) )
6		oveq1	|- ( x = A -> ( x H y ) = ( A H y ) )
7		oveq2	|- ( x = A -> ( y H x ) = ( y H A ) )
8	6 7	eqeq12d	|- ( x = A -> ( ( x H y ) = ( y H x ) <-> ( A H y ) = ( y H A ) ) )
9		oveq2	|- ( y = B -> ( A H y ) = ( A H B ) )
10		oveq1	|- ( y = B -> ( y H A ) = ( B H A ) )
11	9 10	eqeq12d	|- ( y = B -> ( ( A H y ) = ( y H A ) <-> ( A H B ) = ( B H A ) ) )
12	8 11	rspc2v	|- ( ( A e. X /\ B e. X ) -> ( A. x e. X A. y e. X ( x H y ) = ( y H x ) -> ( A H B ) = ( B H A ) ) )
13	5 12	mpan9	|- ( ( R e. CRingOps /\ ( A e. X /\ B e. X ) ) -> ( A H B ) = ( B H A ) )
14	13	3impb	|- ( ( R e. CRingOps /\ A e. X /\ B e. X ) -> ( A H B ) = ( B H A ) )