Theorem mgmhmpropd

Description: Magma homomorphism depends only on the operation of structures. (Contributed by AV, 25-Feb-2020)

	Ref	Expression
Hypotheses	mgmhmpropd.a	$$⊢\phi \to B={\mathrm{Base}}_J$$
	mgmhmpropd.b	$$⊢\phi \to C={\mathrm{Base}}_K$$
	mgmhmpropd.c	$$⊢\phi \to B={\mathrm{Base}}_L$$
	mgmhmpropd.d	$$⊢\phi \to C={\mathrm{Base}}_M$$
	mgmhmpropd.0	$$⊢\phi \to B\ne \varnothing$$
	mgmhmpropd.C	$$⊢\phi \to C\ne \varnothing$$
	mgmhmpropd.e	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{J}y=x{+}_{L}y$$
	mgmhmpropd.f	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in C\right)\right)\to x{+}_{K}y=x{+}_{M}y$$
Assertion	mgmhmpropd	$$⊢\phi \to J\mathrm{MgmHom}K=L\mathrm{MgmHom}M$$

Proof

Step	Hyp	Ref	Expression
1		mgmhmpropd.a	$$⊢\phi \to B={\mathrm{Base}}_J$$
2		mgmhmpropd.b	$$⊢\phi \to C={\mathrm{Base}}_K$$
3		mgmhmpropd.c	$$⊢\phi \to B={\mathrm{Base}}_L$$
4		mgmhmpropd.d	$$⊢\phi \to C={\mathrm{Base}}_M$$
5		mgmhmpropd.0	$$⊢\phi \to B\ne \varnothing$$
6		mgmhmpropd.C	$$⊢\phi \to C\ne \varnothing$$
7		mgmhmpropd.e	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{J}y=x{+}_{L}y$$
8		mgmhmpropd.f	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in C\right)\right)\to x{+}_{K}y=x{+}_{M}y$$
9	7	fveq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to f\left(x{+}_{J}y\right)=f\left(x{+}_{L}y\right)$$
10	9	adantlr	$$⊢\left(\left(\phi \wedge f:B⟶C\right)\wedge \left(x\in B\wedge y\in B\right)\right)\to f\left(x{+}_{J}y\right)=f\left(x{+}_{L}y\right)$$
11		ffvelrn	$$⊢\left(f:B⟶C\wedge x\in B\right)\to f\left(x\right)\in C$$
12		ffvelrn	$$⊢\left(f:B⟶C\wedge y\in B\right)\to f\left(y\right)\in C$$
13	11 12	anim12dan	$$⊢\left(f:B⟶C\wedge \left(x\in B\wedge y\in B\right)\right)\to \left(f\left(x\right)\in C\wedge f\left(y\right)\in C\right)$$
14	8	ralrimivva	$$⊢\phi \to \forall x\in C\forall y\in Cx{+}_{K}y=x{+}_{M}y$$
15		oveq1	$$⊢x=w\to x{+}_{K}y=w{+}_{K}y$$
16		oveq1	$$⊢x=w\to x{+}_{M}y=w{+}_{M}y$$
17	15 16	eqeq12d	$$⊢x=w\to \left(x{+}_{K}y=x{+}_{M}y\leftrightarrow w{+}_{K}y=w{+}_{M}y\right)$$
18		oveq2	$$⊢y=z\to w{+}_{K}y=w{+}_{K}z$$
19		oveq2	$$⊢y=z\to w{+}_{M}y=w{+}_{M}z$$
20	18 19	eqeq12d	$$⊢y=z\to \left(w{+}_{K}y=w{+}_{M}y\leftrightarrow w{+}_{K}z=w{+}_{M}z\right)$$
21	17 20	cbvral2vw	$$⊢\forall x\in C\forall y\in Cx{+}_{K}y=x{+}_{M}y\leftrightarrow \forall w\in C\forall z\in Cw{+}_{K}z=w{+}_{M}z$$
22	14 21	sylib	$$⊢\phi \to \forall w\in C\forall z\in Cw{+}_{K}z=w{+}_{M}z$$
23		oveq1	$$⊢w=f\left(x\right)\to w{+}_{K}z=f\left(x\right){+}_{K}z$$
24		oveq1	$$⊢w=f\left(x\right)\to w{+}_{M}z=f\left(x\right){+}_{M}z$$
25	23 24	eqeq12d	$$⊢w=f\left(x\right)\to \left(w{+}_{K}z=w{+}_{M}z\leftrightarrow f\left(x\right){+}_{K}z=f\left(x\right){+}_{M}z\right)$$
26		oveq2	$$⊢z=f\left(y\right)\to f\left(x\right){+}_{K}z=f\left(x\right){+}_{K}f\left(y\right)$$
27		oveq2	$$⊢z=f\left(y\right)\to f\left(x\right){+}_{M}z=f\left(x\right){+}_{M}f\left(y\right)$$
28	26 27	eqeq12d	$$⊢z=f\left(y\right)\to \left(f\left(x\right){+}_{K}z=f\left(x\right){+}_{M}z\leftrightarrow f\left(x\right){+}_{K}f\left(y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)$$
29	25 28	rspc2va	$$⊢\left(\left(f\left(x\right)\in C\wedge f\left(y\right)\in C\right)\wedge \forall w\in C\forall z\in Cw{+}_{K}z=w{+}_{M}z\right)\to f\left(x\right){+}_{K}f\left(y\right)=f\left(x\right){+}_{M}f\left(y\right)$$
30	13 22 29	syl2anr	$$⊢\left(\phi \wedge \left(f:B⟶C\wedge \left(x\in B\wedge y\in B\right)\right)\right)\to f\left(x\right){+}_{K}f\left(y\right)=f\left(x\right){+}_{M}f\left(y\right)$$
31	30	anassrs	$$⊢\left(\left(\phi \wedge f:B⟶C\right)\wedge \left(x\in B\wedge y\in B\right)\right)\to f\left(x\right){+}_{K}f\left(y\right)=f\left(x\right){+}_{M}f\left(y\right)$$
32	10 31	eqeq12d	$$⊢\left(\left(\phi \wedge f:B⟶C\right)\wedge \left(x\in B\wedge y\in B\right)\right)\to \left(f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\leftrightarrow f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)$$
33	32	2ralbidva	$$⊢\left(\phi \wedge f:B⟶C\right)\to \left(\forall x\in B\forall y\in Bf\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\leftrightarrow \forall x\in B\forall y\in Bf\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)$$
34	33	adantrl	$$⊢\left(\phi \wedge \left(\left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\wedge f:B⟶C\right)\right)\to \left(\forall x\in B\forall y\in Bf\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\leftrightarrow \forall x\in B\forall y\in Bf\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)$$
35		raleq	$$⊢B={\mathrm{Base}}_J\to \left(\forall y\in Bf\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\leftrightarrow \forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\right)$$
36	35	raleqbi1dv	$$⊢B={\mathrm{Base}}_J\to \left(\forall x\in B\forall y\in Bf\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\leftrightarrow \forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\right)$$
37	1 36	syl	$$⊢\phi \to \left(\forall x\in B\forall y\in Bf\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\leftrightarrow \forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\right)$$
38	37	adantr	$$⊢\left(\phi \wedge \left(\left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\wedge f:B⟶C\right)\right)\to \left(\forall x\in B\forall y\in Bf\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\leftrightarrow \forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\right)$$
39		raleq	$$⊢B={\mathrm{Base}}_L\to \left(\forall y\in Bf\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\leftrightarrow \forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)$$
40	39	raleqbi1dv	$$⊢B={\mathrm{Base}}_L\to \left(\forall x\in B\forall y\in Bf\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)$$
41	3 40	syl	$$⊢\phi \to \left(\forall x\in B\forall y\in Bf\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)$$
42	41	adantr	$$⊢\left(\phi \wedge \left(\left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\wedge f:B⟶C\right)\right)\to \left(\forall x\in B\forall y\in Bf\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)$$
43	34 38 42	3bitr3d	$$⊢\left(\phi \wedge \left(\left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\wedge f:B⟶C\right)\right)\to \left(\forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)$$
44	43	anassrs	$$⊢\left(\left(\phi \wedge \left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\right)\wedge f:B⟶C\right)\to \left(\forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)$$
45	44	pm5.32da	$$⊢\left(\phi \wedge \left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\right)\to \left(\left(f:B⟶C\wedge \forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\right)\leftrightarrow \left(f:B⟶C\wedge \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)\right)$$
46	1 2	feq23d	$$⊢\phi \to \left(f:B⟶C\leftrightarrow f:{\mathrm{Base}}_J⟶{\mathrm{Base}}_K\right)$$
47	46	adantr	$$⊢\left(\phi \wedge \left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\right)\to \left(f:B⟶C\leftrightarrow f:{\mathrm{Base}}_J⟶{\mathrm{Base}}_K\right)$$
48	47	anbi1d	$$⊢\left(\phi \wedge \left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\right)\to \left(\left(f:B⟶C\wedge \forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\right)\leftrightarrow \left(f:{\mathrm{Base}}_J⟶{\mathrm{Base}}_K\wedge \forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\right)\right)$$
49	3 4	feq23d	$$⊢\phi \to \left(f:B⟶C\leftrightarrow f:{\mathrm{Base}}_L⟶{\mathrm{Base}}_M\right)$$
50	49	adantr	$$⊢\left(\phi \wedge \left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\right)\to \left(f:B⟶C\leftrightarrow f:{\mathrm{Base}}_L⟶{\mathrm{Base}}_M\right)$$
51	50	anbi1d	$$⊢\left(\phi \wedge \left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\right)\to \left(\left(f:B⟶C\wedge \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)\leftrightarrow \left(f:{\mathrm{Base}}_L⟶{\mathrm{Base}}_M\wedge \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)\right)$$
52	45 48 51	3bitr3d	$$⊢\left(\phi \wedge \left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\right)\to \left(\left(f:{\mathrm{Base}}_J⟶{\mathrm{Base}}_K\wedge \forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\right)\leftrightarrow \left(f:{\mathrm{Base}}_L⟶{\mathrm{Base}}_M\wedge \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)\right)$$
53	52	pm5.32da	$$⊢\phi \to \left(\left(\left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\wedge \left(f:{\mathrm{Base}}_J⟶{\mathrm{Base}}_K\wedge \forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\right)\right)\leftrightarrow \left(\left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\wedge \left(f:{\mathrm{Base}}_L⟶{\mathrm{Base}}_M\wedge \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)\right)\right)$$
54	1 3 5 7	mgmpropd	$$⊢\phi \to \left(J\in \mathrm{Mgm}\leftrightarrow L\in \mathrm{Mgm}\right)$$
55	2 4 6 8	mgmpropd	$$⊢\phi \to \left(K\in \mathrm{Mgm}\leftrightarrow M\in \mathrm{Mgm}\right)$$
56	54 55	anbi12d	$$⊢\phi \to \left(\left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\leftrightarrow \left(L\in \mathrm{Mgm}\wedge M\in \mathrm{Mgm}\right)\right)$$
57	56	anbi1d	$$⊢\phi \to \left(\left(\left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\wedge \left(f:{\mathrm{Base}}_L⟶{\mathrm{Base}}_M\wedge \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)\right)\leftrightarrow \left(\left(L\in \mathrm{Mgm}\wedge M\in \mathrm{Mgm}\right)\wedge \left(f:{\mathrm{Base}}_L⟶{\mathrm{Base}}_M\wedge \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)\right)\right)$$
58	53 57	bitrd	$$⊢\phi \to \left(\left(\left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\wedge \left(f:{\mathrm{Base}}_J⟶{\mathrm{Base}}_K\wedge \forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\right)\right)\leftrightarrow \left(\left(L\in \mathrm{Mgm}\wedge M\in \mathrm{Mgm}\right)\wedge \left(f:{\mathrm{Base}}_L⟶{\mathrm{Base}}_M\wedge \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)\right)\right)$$
59		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
60		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
61		eqid	$$⊢{+}_J={+}_J$$
62		eqid	$$⊢{+}_K={+}_K$$
63	59 60 61 62	ismgmhm	$$⊢f\in \left(J\mathrm{MgmHom}K\right)\leftrightarrow \left(\left(J\in \mathrm{Mgm}\wedge K\in \mathrm{Mgm}\right)\wedge \left(f:{\mathrm{Base}}_J⟶{\mathrm{Base}}_K\wedge \forall x\in {\mathrm{Base}}_J\forall y\in {\mathrm{Base}}_{J}f\left(x{+}_{J}y\right)=f\left(x\right){+}_{K}f\left(y\right)\right)\right)$$
64		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
65		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
66		eqid	$$⊢{+}_L={+}_L$$
67		eqid	$$⊢{+}_M={+}_M$$
68	64 65 66 67	ismgmhm	$$⊢f\in \left(L\mathrm{MgmHom}M\right)\leftrightarrow \left(\left(L\in \mathrm{Mgm}\wedge M\in \mathrm{Mgm}\right)\wedge \left(f:{\mathrm{Base}}_L⟶{\mathrm{Base}}_M\wedge \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}f\left(x{+}_{L}y\right)=f\left(x\right){+}_{M}f\left(y\right)\right)\right)$$
69	58 63 68	3bitr4g	$$⊢\phi \to \left(f\in \left(J\mathrm{MgmHom}K\right)\leftrightarrow f\in \left(L\mathrm{MgmHom}M\right)\right)$$
70	69	eqrdv	$$⊢\phi \to J\mathrm{MgmHom}K=L\mathrm{MgmHom}M$$