Metamath Proof Explorer

Theorem rngosm

Description: Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	ringi.1	$⊢ G = 1^{st} (R)$
		ringi.2	$⊢ H = 2^{nd} (R)$
		ringi.3	$⊢ X = ran G$
	Assertion	rngosm	$⊢ R \in RingOps \to H : X \times X ⟶ X$

Proof

Step	Hyp	Ref	Expression
1		ringi.1	$⊢ G = 1^{st} (R)$
2		ringi.2	$⊢ H = 2^{nd} (R)$
3		ringi.3	$⊢ X = ran G$
4	1 2 3	rngoi	$⊢ R \in RingOps \to ((G \in AbelOp \land H : X \times X ⟶ X) \land (\forall x \in X \forall y \in X \forall z \in X ((x H y) H z = x H (y H z) \land x H (y G z) = (x H y) G (x H z) \land (x G y) H z = (x H z) G (y H z)) \land \exists x \in X \forall y \in X (x H y = y \land y H x = y)))$
5	4	simpld	$⊢ R \in RingOps \to (G \in AbelOp \land H : X \times X ⟶ X)$
6	5	simprd	$⊢ R \in RingOps \to H : X \times X ⟶ X$