Metamath Proof Explorer

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 = 2^{nd} (R)$
	rnplrnml0.2	$⊢ G = 1^{st} (R)$
Assertion	rngorn1	$⊢ R \in RingOps \to ran G = dom dom H$

Proof

Step	Hyp	Ref	Expression
1		rnplrnml0.1	$⊢ H = 2^{nd} (R)$
2		rnplrnml0.2	$⊢ G = 1^{st} (R)$
3	2	rngogrpo	$⊢ R \in RingOps \to G \in GrpOp$
4		grporndm	$⊢ G \in GrpOp \to ran G = dom dom G$
5	3 4	syl	$⊢ R \in RingOps \to ran G = dom dom G$
6	1 2	rngodm1dm2	$⊢ R \in RingOps \to dom dom G = dom dom H$
7	5 6	eqtrd	$⊢ R \in RingOps \to ran G = dom dom H$