Metamath Proof Explorer

Theorem isrngod

Description: Conditions that determine a ring. (Changed label from isringd to isrngod -NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses isringod.1 ${⊢}{\phi }\to {G}\in \mathrm{AbelOp}$
isringod.2 ${⊢}{\phi }\to {X}=\mathrm{ran}{G}$
isringod.3 ${⊢}{\phi }\to {H}:{X}×{X}⟶{X}$
isringod.4 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\wedge {z}\in {X}\right)\right)\to \left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)$
isringod.5 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\wedge {z}\in {X}\right)\right)\to {x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)$
isringod.6 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\wedge {z}\in {X}\right)\right)\to \left({x}{G}{y}\right){H}{z}=\left({x}{H}{z}\right){G}\left({y}{H}{z}\right)$
isringod.7 ${⊢}{\phi }\to {U}\in {X}$
isringod.8 ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {U}{H}{y}={y}$
isringod.9 ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {y}{H}{U}={y}$
Assertion isrngod ${⊢}{\phi }\to ⟨{G},{H}⟩\in \mathrm{RingOps}$

Proof

Step Hyp Ref Expression
1 isringod.1 ${⊢}{\phi }\to {G}\in \mathrm{AbelOp}$
2 isringod.2 ${⊢}{\phi }\to {X}=\mathrm{ran}{G}$
3 isringod.3 ${⊢}{\phi }\to {H}:{X}×{X}⟶{X}$
4 isringod.4 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\wedge {z}\in {X}\right)\right)\to \left({x}{H}{y}\right){H}{z}={x}{H}\left({y}{H}{z}\right)$
5 isringod.5 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\wedge {z}\in {X}\right)\right)\to {x}{H}\left({y}{G}{z}\right)=\left({x}{H}{y}\right){G}\left({x}{H}{z}\right)$
6 isringod.6 ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\wedge {z}\in {X}\right)\right)\to \left({x}{G}{y}\right){H}{z}=\left({x}{H}{z}\right){G}\left({y}{H}{z}\right)$
7 isringod.7 ${⊢}{\phi }\to {U}\in {X}$
8 isringod.8 ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {U}{H}{y}={y}$
9 isringod.9 ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to {y}{H}{U}={y}$
10 2 sqxpeqd ${⊢}{\phi }\to {X}×{X}=\mathrm{ran}{G}×\mathrm{ran}{G}$
11 10 2 feq23d ${⊢}{\phi }\to \left({H}:{X}×{X}⟶{X}↔{H}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\right)$
12 3 11 mpbid ${⊢}{\phi }\to {H}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}$
13 4 5 6 3jca ${⊢}\left({\phi }\wedge \left({x}\in {X}\wedge {y}\in {X}\wedge {z}\in {X}\right)\right)\to \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)$
14 13 ralrimivvva ${⊢}{\phi }\to \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)$
15 2 raleqdv ${⊢}{\phi }\to \left(\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)↔\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)\right)$
16 2 15 raleqbidv ${⊢}{\phi }\to \left(\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)↔\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)\right)$
17 2 16 raleqbidv ${⊢}{\phi }\to \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)↔\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)\right)$
18 14 17 mpbid ${⊢}{\phi }\to \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)$
19 8 9 jca ${⊢}\left({\phi }\wedge {y}\in {X}\right)\to \left({U}{H}{y}={y}\wedge {y}{H}{U}={y}\right)$
20 19 ralrimiva ${⊢}{\phi }\to \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({U}{H}{y}={y}\wedge {y}{H}{U}={y}\right)$
21 oveq1 ${⊢}{x}={U}\to {x}{H}{y}={U}{H}{y}$
22 21 eqeq1d ${⊢}{x}={U}\to \left({x}{H}{y}={y}↔{U}{H}{y}={y}\right)$
23 22 ovanraleqv ${⊢}{x}={U}\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({U}{H}{y}={y}\wedge {y}{H}{U}={y}\right)\right)$
24 23 rspcev ${⊢}\left({U}\in {X}\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({U}{H}{y}={y}\wedge {y}{H}{U}={y}\right)\right)\to \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)$
25 7 20 24 syl2anc ${⊢}{\phi }\to \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)$
26 2 raleqdv ${⊢}{\phi }\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)↔\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{H}{y}={y}\wedge {y}{H}{x}={y}\right)\right)$
27 2 26 rexeqbidv ${⊢}{\phi }\to \left(\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)↔\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)$
28 25 27 mpbid ${⊢}{\phi }\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)$
29 18 28 jca ${⊢}{\phi }\to \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)$
30 1 12 29 jca31 ${⊢}{\phi }\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)$
31 rnexg ${⊢}{G}\in \mathrm{AbelOp}\to \mathrm{ran}{G}\in \mathrm{V}$
32 1 31 syl ${⊢}{\phi }\to \mathrm{ran}{G}\in \mathrm{V}$
33 32 32 xpexd ${⊢}{\phi }\to \mathrm{ran}{G}×\mathrm{ran}{G}\in \mathrm{V}$
34 fex ${⊢}\left({H}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\wedge \mathrm{ran}{G}×\mathrm{ran}{G}\in \mathrm{V}\right)\to {H}\in \mathrm{V}$
35 12 33 34 syl2anc ${⊢}{\phi }\to {H}\in \mathrm{V}$
36 eqid ${⊢}\mathrm{ran}{G}=\mathrm{ran}{G}$
37 36 isrngo ${⊢}{H}\in \mathrm{V}\to \left(⟨{G},{H}⟩\in \mathrm{RingOps}↔\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)\right)$
38 35 37 syl ${⊢}{\phi }\to \left(⟨{G},{H}⟩\in \mathrm{RingOps}↔\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)\right)$
39 30 38 mpbird ${⊢}{\phi }\to ⟨{G},{H}⟩\in \mathrm{RingOps}$