Metamath Proof Explorer

Theorem rngorn1eq

Description: In a unital ring the range of the addition equals the range 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	rngorn1eq	$⊢ R \in RingOps \to ran G = ran H$

Proof

Step	Hyp	Ref	Expression
1		rnplrnml0.1	$⊢ H = 2^{nd} (R)$
2		rnplrnml0.2	$⊢ G = 1^{st} (R)$
3		eqid	$⊢ ran G = ran G$
4	2 1 3	rngosm	$⊢ R \in RingOps \to H : ran G \times ran G ⟶ ran G$
5	2 1 3	rngoi	$⊢ R \in RingOps \to ((G \in AbelOp \land H : ran G \times ran G ⟶ ran G) \land (\forall x \in ran G \forall y \in ran G \forall z \in ran G ((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 ran G \forall y \in ran G (x H y = y \land y H x = y)))$
6	5	simprrd	$⊢ R \in RingOps \to \exists x \in ran G \forall y \in ran G (x H y = y \land y H x = y)$
7		rngmgmbs4	$⊢ (H : ran G \times ran G ⟶ ran G \land \exists x \in ran G \forall y \in ran G (x H y = y \land y H x = y)) \to ran H = ran G$
8	4 6 7	syl2anc	$⊢ R \in RingOps \to ran H = ran G$
9	8	eqcomd	$⊢ R \in RingOps \to ran G = ran H$