# Metamath Proof Explorer

## Theorem rngoi

Description: The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007) (Proof shortened by Mario Carneiro, 21-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 rngoi ${⊢}{R}\in \mathrm{RingOps}\to \left(\left({G}\in \mathrm{AbelOp}\wedge {H}:{X}×{X}⟶{X}\right)\wedge \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\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 {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)\right)\right)$

### 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 relrngo ${⊢}\mathrm{Rel}\mathrm{RingOps}$
5 1st2nd ${⊢}\left(\mathrm{Rel}\mathrm{RingOps}\wedge {R}\in \mathrm{RingOps}\right)\to {R}=⟨{1}^{st}\left({R}\right),{2}^{nd}\left({R}\right)⟩$
6 4 5 mpan ${⊢}{R}\in \mathrm{RingOps}\to {R}=⟨{1}^{st}\left({R}\right),{2}^{nd}\left({R}\right)⟩$
7 1 2 opeq12i ${⊢}⟨{G},{H}⟩=⟨{1}^{st}\left({R}\right),{2}^{nd}\left({R}\right)⟩$
8 6 7 syl6reqr ${⊢}{R}\in \mathrm{RingOps}\to ⟨{G},{H}⟩={R}$
9 id ${⊢}{R}\in \mathrm{RingOps}\to {R}\in \mathrm{RingOps}$
10 8 9 eqeltrd ${⊢}{R}\in \mathrm{RingOps}\to ⟨{G},{H}⟩\in \mathrm{RingOps}$
11 2 fvexi ${⊢}{H}\in \mathrm{V}$
12 3 isrngo ${⊢}{H}\in \mathrm{V}\to \left(⟨{G},{H}⟩\in \mathrm{RingOps}↔\left(\left({G}\in \mathrm{AbelOp}\wedge {H}:{X}×{X}⟶{X}\right)\wedge \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\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 {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)\right)\right)\right)$
13 11 12 ax-mp ${⊢}⟨{G},{H}⟩\in \mathrm{RingOps}↔\left(\left({G}\in \mathrm{AbelOp}\wedge {H}:{X}×{X}⟶{X}\right)\wedge \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\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 {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)\right)\right)$
14 10 13 sylib ${⊢}{R}\in \mathrm{RingOps}\to \left(\left({G}\in \mathrm{AbelOp}\wedge {H}:{X}×{X}⟶{X}\right)\wedge \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\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 {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)\right)\right)$