# 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}\left({R}\right)$
rnplrnml0.2 ${⊢}{G}={1}^{st}\left({R}\right)$
Assertion rngorn1eq ${⊢}{R}\in \mathrm{RingOps}\to \mathrm{ran}{G}=\mathrm{ran}{H}$

### Proof

Step Hyp Ref Expression
1 rnplrnml0.1 ${⊢}{H}={2}^{nd}\left({R}\right)$
2 rnplrnml0.2 ${⊢}{G}={1}^{st}\left({R}\right)$
3 eqid ${⊢}\mathrm{ran}{G}=\mathrm{ran}{G}$
4 2 1 3 rngosm ${⊢}{R}\in \mathrm{RingOps}\to {H}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}$
5 2 1 3 rngoi ${⊢}{R}\in \mathrm{RingOps}\to \left(\left({G}\in \mathrm{AbelOp}\wedge {H}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\right)\wedge \left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left(\left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)\wedge {x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)\wedge \left({x}{G}{y}\right){H}{z}=\left({x}{H}{z}\right){G}\left({y}{H}{z}\right)\right)\wedge \exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)\right)\right)$
6 5 simprrd ${⊢}{R}\in \mathrm{RingOps}\to \exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)$
7 rngmgmbs4 ${⊢}\left({H}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\wedge \exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)\right)\to \mathrm{ran}{H}=\mathrm{ran}{G}$
8 4 6 7 syl2anc ${⊢}{R}\in \mathrm{RingOps}\to \mathrm{ran}{H}=\mathrm{ran}{G}$
9 8 eqcomd ${⊢}{R}\in \mathrm{RingOps}\to \mathrm{ran}{G}=\mathrm{ran}{H}$