Theorem rngosm

Description: Obsolete theorem. 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.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ringi.1	$$⊢G=1^{st}\left(R\right)$$
2		ringi.2	$$⊢H=2^{nd}\left(R\right)$$
3		ringi.3	$$⊢X=\mathrm{ran}G$$
4	1 2 3	rngoi	$$⊢R\in \mathrm{RingOps}\to \left(\left(G\in \mathrm{AbelOp}\wedge H:X\times X⟶X\right)\wedge \left(\forall x\in X\forall y\in X\forall z\in X\left(\left(xHy\right)Hz=xH\left(yHz\right)\wedge xH\left(yGz\right)=\left(xHy\right)G\left(xHz\right)\wedge \left(xGy\right)Hz=\left(xHz\right)G\left(yHz\right)\right)\wedge \exists x\in X\forall y\in X\left(xHy=y\wedge yHx=y\right)\right)\right)$$
5	4	simpld	$$⊢R\in \mathrm{RingOps}\to \left(G\in \mathrm{AbelOp}\wedge H:X\times X⟶X\right)$$
6	5	simprd	$$⊢R\in \mathrm{RingOps}\to H:X\times X⟶X$$