# Metamath Proof Explorer

## Theorem rngo2

Description: A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 22-Dec-2013) (New usage 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 rngo2 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{A}{G}{A}=\left({x}{G}{x}\right){H}{A}$

### 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 rngoid ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{A}={A}\wedge {A}{H}{x}={A}\right)$
5 oveq12 ${⊢}\left({x}{H}{A}={A}\wedge {x}{H}{A}={A}\right)\to \left({x}{H}{A}\right){G}\left({x}{H}{A}\right)={A}{G}{A}$
6 5 anidms ${⊢}{x}{H}{A}={A}\to \left({x}{H}{A}\right){G}\left({x}{H}{A}\right)={A}{G}{A}$
7 6 eqcomd ${⊢}{x}{H}{A}={A}\to {A}{G}{A}=\left({x}{H}{A}\right){G}\left({x}{H}{A}\right)$
8 simpll ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\wedge {x}\in {X}\right)\to {R}\in \mathrm{RingOps}$
9 simpr ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\wedge {x}\in {X}\right)\to {x}\in {X}$
10 simplr ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\wedge {x}\in {X}\right)\to {A}\in {X}$
11 1 2 3 rngodir ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({x}\in {X}\wedge {x}\in {X}\wedge {A}\in {X}\right)\right)\to \left({x}{G}{x}\right){H}{A}=\left({x}{H}{A}\right){G}\left({x}{H}{A}\right)$
12 8 9 9 10 11 syl13anc ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\wedge {x}\in {X}\right)\to \left({x}{G}{x}\right){H}{A}=\left({x}{H}{A}\right){G}\left({x}{H}{A}\right)$
13 12 eqeq2d ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\wedge {x}\in {X}\right)\to \left({A}{G}{A}=\left({x}{G}{x}\right){H}{A}↔{A}{G}{A}=\left({x}{H}{A}\right){G}\left({x}{H}{A}\right)\right)$
14 7 13 syl5ibr ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\wedge {x}\in {X}\right)\to \left({x}{H}{A}={A}\to {A}{G}{A}=\left({x}{G}{x}\right){H}{A}\right)$
15 14 adantrd ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\wedge {x}\in {X}\right)\to \left(\left({x}{H}{A}={A}\wedge {A}{H}{x}={A}\right)\to {A}{G}{A}=\left({x}{G}{x}\right){H}{A}\right)$
16 15 reximdva ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \left(\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{A}={A}\wedge {A}{H}{x}={A}\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{A}{G}{A}=\left({x}{G}{x}\right){H}{A}\right)$
17 4 16 mpd ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{A}{G}{A}=\left({x}{G}{x}\right){H}{A}$