Metamath Proof Explorer

Theorem crngocom

Description: Obsolete theorem, use crngcom instead. The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	crngocom.1	$⊢ G = 1^{st} (R)$
		crngocom.2	$⊢ H = 2^{nd} (R)$
		crngocom.3	$⊢ X = ran G$
	Assertion	crngocom	$⊢ (R \in CRingOps \land A \in X \land B \in X) \to A H B = B H A$

Proof

Step	Hyp	Ref	Expression
1		crngocom.1	$⊢ G = 1^{st} (R)$
2		crngocom.2	$⊢ H = 2^{nd} (R)$
3		crngocom.3	$⊢ X = ran G$
4	1 2 3	iscrngo2	$⊢ R \in CRingOps \leftrightarrow (R \in RingOps \land \forall x \in X \forall y \in X x H y = y H x)$
5	4	simprbi	$⊢ R \in CRingOps \to \forall x \in X \forall y \in X x H y = y H x$
6		oveq1	$⊢ x = A \to x H y = A H y$
7		oveq2	$⊢ x = A \to y H x = y H A$
8	6 7	eqeq12d	$⊢ x = A \to (x H y = y H x \leftrightarrow A H y = y H A)$
9		oveq2	$⊢ y = B \to A H y = A H B$
10		oveq1	$⊢ y = B \to y H A = B H A$
11	9 10	eqeq12d	$⊢ y = B \to (A H y = y H A \leftrightarrow A H B = B H A)$
12	8 11	rspc2v	$⊢ (A \in X \land B \in X) \to (\forall x \in X \forall y \in X x H y = y H x \to A H B = B H A)$
13	5 12	mpan9	$⊢ (R \in CRingOps \land (A \in X \land B \in X)) \to A H B = B H A$
14	13	3impb	$⊢ (R \in CRingOps \land A \in X \land B \in X) \to A H B = B H A$