Theorem rngorn1

Description: In a unital ring the range of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rnplrnml0.1	|- H = ( 2nd ` R )
	rnplrnml0.2	|- G = ( 1st ` R )
Assertion	rngorn1	|- ( R e. RingOps -> ran G = dom dom H )

Proof

Step	Hyp	Ref	Expression
1		rnplrnml0.1	|- H = ( 2nd ` R )
2		rnplrnml0.2	|- G = ( 1st ` R )
3	2	rngogrpo	|- ( R e. RingOps -> G e. GrpOp )
4		grporndm	|- ( G e. GrpOp -> ran G = dom dom G )
5	3 4	syl	|- ( R e. RingOps -> ran G = dom dom G )
6	1 2	rngodm1dm2	|- ( R e. RingOps -> dom dom G = dom dom H )
7	5 6	eqtrd	|- ( R e. RingOps -> ran G = dom dom H )