# Metamath Proof Explorer

## Theorem rhmpropd

Description: Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses rhmpropd.a ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{J}}$
rhmpropd.b ${⊢}{\phi }\to {C}={\mathrm{Base}}_{{K}}$
rhmpropd.c ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{L}}$
rhmpropd.d ${⊢}{\phi }\to {C}={\mathrm{Base}}_{{M}}$
rhmpropd.e ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{+}_{{J}}{y}={x}{+}_{{L}}{y}$
rhmpropd.f ${⊢}\left({\phi }\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}{+}_{{K}}{y}={x}{+}_{{M}}{y}$
rhmpropd.g ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{J}}{y}={x}{\cdot }_{{L}}{y}$
rhmpropd.h ${⊢}\left({\phi }\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}{\cdot }_{{K}}{y}={x}{\cdot }_{{M}}{y}$
Assertion rhmpropd ${⊢}{\phi }\to {J}\mathrm{RingHom}{K}={L}\mathrm{RingHom}{M}$

### Proof

Step Hyp Ref Expression
1 rhmpropd.a ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{J}}$
2 rhmpropd.b ${⊢}{\phi }\to {C}={\mathrm{Base}}_{{K}}$
3 rhmpropd.c ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{L}}$
4 rhmpropd.d ${⊢}{\phi }\to {C}={\mathrm{Base}}_{{M}}$
5 rhmpropd.e ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{+}_{{J}}{y}={x}{+}_{{L}}{y}$
6 rhmpropd.f ${⊢}\left({\phi }\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}{+}_{{K}}{y}={x}{+}_{{M}}{y}$
7 rhmpropd.g ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{J}}{y}={x}{\cdot }_{{L}}{y}$
8 rhmpropd.h ${⊢}\left({\phi }\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}{\cdot }_{{K}}{y}={x}{\cdot }_{{M}}{y}$
9 1 3 5 7 ringpropd ${⊢}{\phi }\to \left({J}\in \mathrm{Ring}↔{L}\in \mathrm{Ring}\right)$
10 2 4 6 8 ringpropd ${⊢}{\phi }\to \left({K}\in \mathrm{Ring}↔{M}\in \mathrm{Ring}\right)$
11 9 10 anbi12d ${⊢}{\phi }\to \left(\left({J}\in \mathrm{Ring}\wedge {K}\in \mathrm{Ring}\right)↔\left({L}\in \mathrm{Ring}\wedge {M}\in \mathrm{Ring}\right)\right)$
12 1 2 3 4 5 6 ghmpropd ${⊢}{\phi }\to {J}\mathrm{GrpHom}{K}={L}\mathrm{GrpHom}{M}$
13 12 eleq2d ${⊢}{\phi }\to \left({f}\in \left({J}\mathrm{GrpHom}{K}\right)↔{f}\in \left({L}\mathrm{GrpHom}{M}\right)\right)$
14 eqid ${⊢}{\mathrm{mulGrp}}_{{J}}={\mathrm{mulGrp}}_{{J}}$
15 eqid ${⊢}{\mathrm{Base}}_{{J}}={\mathrm{Base}}_{{J}}$
16 14 15 mgpbas ${⊢}{\mathrm{Base}}_{{J}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{J}}}$
17 1 16 syl6eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{J}}}$
18 eqid ${⊢}{\mathrm{mulGrp}}_{{K}}={\mathrm{mulGrp}}_{{K}}$
19 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
20 18 19 mgpbas ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{K}}}$
21 2 20 syl6eq ${⊢}{\phi }\to {C}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{K}}}$
22 eqid ${⊢}{\mathrm{mulGrp}}_{{L}}={\mathrm{mulGrp}}_{{L}}$
23 eqid ${⊢}{\mathrm{Base}}_{{L}}={\mathrm{Base}}_{{L}}$
24 22 23 mgpbas ${⊢}{\mathrm{Base}}_{{L}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{L}}}$
25 3 24 syl6eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{L}}}$
26 eqid ${⊢}{\mathrm{mulGrp}}_{{M}}={\mathrm{mulGrp}}_{{M}}$
27 eqid ${⊢}{\mathrm{Base}}_{{M}}={\mathrm{Base}}_{{M}}$
28 26 27 mgpbas ${⊢}{\mathrm{Base}}_{{M}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{M}}}$
29 4 28 syl6eq ${⊢}{\phi }\to {C}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{M}}}$
30 eqid ${⊢}{\cdot }_{{J}}={\cdot }_{{J}}$
31 14 30 mgpplusg ${⊢}{\cdot }_{{J}}={+}_{{\mathrm{mulGrp}}_{{J}}}$
32 31 oveqi ${⊢}{x}{\cdot }_{{J}}{y}={x}{+}_{{\mathrm{mulGrp}}_{{J}}}{y}$
33 eqid ${⊢}{\cdot }_{{L}}={\cdot }_{{L}}$
34 22 33 mgpplusg ${⊢}{\cdot }_{{L}}={+}_{{\mathrm{mulGrp}}_{{L}}}$
35 34 oveqi ${⊢}{x}{\cdot }_{{L}}{y}={x}{+}_{{\mathrm{mulGrp}}_{{L}}}{y}$
36 7 32 35 3eqtr3g ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{+}_{{\mathrm{mulGrp}}_{{J}}}{y}={x}{+}_{{\mathrm{mulGrp}}_{{L}}}{y}$
37 eqid ${⊢}{\cdot }_{{K}}={\cdot }_{{K}}$
38 18 37 mgpplusg ${⊢}{\cdot }_{{K}}={+}_{{\mathrm{mulGrp}}_{{K}}}$
39 38 oveqi ${⊢}{x}{\cdot }_{{K}}{y}={x}{+}_{{\mathrm{mulGrp}}_{{K}}}{y}$
40 eqid ${⊢}{\cdot }_{{M}}={\cdot }_{{M}}$
41 26 40 mgpplusg ${⊢}{\cdot }_{{M}}={+}_{{\mathrm{mulGrp}}_{{M}}}$
42 41 oveqi ${⊢}{x}{\cdot }_{{M}}{y}={x}{+}_{{\mathrm{mulGrp}}_{{M}}}{y}$
43 8 39 42 3eqtr3g ${⊢}\left({\phi }\wedge \left({x}\in {C}\wedge {y}\in {C}\right)\right)\to {x}{+}_{{\mathrm{mulGrp}}_{{K}}}{y}={x}{+}_{{\mathrm{mulGrp}}_{{M}}}{y}$
44 17 21 25 29 36 43 mhmpropd ${⊢}{\phi }\to {\mathrm{mulGrp}}_{{J}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{K}}={\mathrm{mulGrp}}_{{L}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{M}}$
45 44 eleq2d ${⊢}{\phi }\to \left({f}\in \left({\mathrm{mulGrp}}_{{J}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{K}}\right)↔{f}\in \left({\mathrm{mulGrp}}_{{L}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{M}}\right)\right)$
46 13 45 anbi12d ${⊢}{\phi }\to \left(\left({f}\in \left({J}\mathrm{GrpHom}{K}\right)\wedge {f}\in \left({\mathrm{mulGrp}}_{{J}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{K}}\right)\right)↔\left({f}\in \left({L}\mathrm{GrpHom}{M}\right)\wedge {f}\in \left({\mathrm{mulGrp}}_{{L}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{M}}\right)\right)\right)$
47 11 46 anbi12d ${⊢}{\phi }\to \left(\left(\left({J}\in \mathrm{Ring}\wedge {K}\in \mathrm{Ring}\right)\wedge \left({f}\in \left({J}\mathrm{GrpHom}{K}\right)\wedge {f}\in \left({\mathrm{mulGrp}}_{{J}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{K}}\right)\right)\right)↔\left(\left({L}\in \mathrm{Ring}\wedge {M}\in \mathrm{Ring}\right)\wedge \left({f}\in \left({L}\mathrm{GrpHom}{M}\right)\wedge {f}\in \left({\mathrm{mulGrp}}_{{L}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{M}}\right)\right)\right)\right)$
48 14 18 isrhm ${⊢}{f}\in \left({J}\mathrm{RingHom}{K}\right)↔\left(\left({J}\in \mathrm{Ring}\wedge {K}\in \mathrm{Ring}\right)\wedge \left({f}\in \left({J}\mathrm{GrpHom}{K}\right)\wedge {f}\in \left({\mathrm{mulGrp}}_{{J}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{K}}\right)\right)\right)$
49 22 26 isrhm ${⊢}{f}\in \left({L}\mathrm{RingHom}{M}\right)↔\left(\left({L}\in \mathrm{Ring}\wedge {M}\in \mathrm{Ring}\right)\wedge \left({f}\in \left({L}\mathrm{GrpHom}{M}\right)\wedge {f}\in \left({\mathrm{mulGrp}}_{{L}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{M}}\right)\right)\right)$
50 47 48 49 3bitr4g ${⊢}{\phi }\to \left({f}\in \left({J}\mathrm{RingHom}{K}\right)↔{f}\in \left({L}\mathrm{RingHom}{M}\right)\right)$
51 50 eqrdv ${⊢}{\phi }\to {J}\mathrm{RingHom}{K}={L}\mathrm{RingHom}{M}$