Theorem mgmpropd

Description: If two structures have the same (nonempty) base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a magma iff the other one is. (Contributed by AV, 25-Feb-2020)

	Ref	Expression
Hypotheses	mgmpropd.k	$$⊢\phi \to B={\mathrm{Base}}_K$$
	mgmpropd.l	$$⊢\phi \to B={\mathrm{Base}}_L$$
	mgmpropd.b	$$⊢\phi \to B\ne \varnothing$$
	mgmpropd.p	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
Assertion	mgmpropd	$$⊢\phi \to \left(K\in \mathrm{Mgm}\leftrightarrow L\in \mathrm{Mgm}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mgmpropd.k	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		mgmpropd.l	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		mgmpropd.b	$$⊢\phi \to B\ne \varnothing$$
4		mgmpropd.p	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
5		simpl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to \phi$$
6	1	eqcomd	$$⊢\phi \to {\mathrm{Base}}_K=B$$
7	6	eleq2d	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K\leftrightarrow x\in B\right)$$
8	7	biimpcd	$$⊢x\in {\mathrm{Base}}_K\to \left(\phi \to x\in B\right)$$
9	8	adantr	$$⊢\left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\to \left(\phi \to x\in B\right)$$
10	9	impcom	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to x\in B$$
11	6	eleq2d	$$⊢\phi \to \left(y\in {\mathrm{Base}}_K\leftrightarrow y\in B\right)$$
12	11	biimpd	$$⊢\phi \to \left(y\in {\mathrm{Base}}_K\to y\in B\right)$$
13	12	adantld	$$⊢\phi \to \left(\left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\to y\in B\right)$$
14	13	imp	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to y\in B$$
15	5 10 14 4	syl12anc	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
16	15	eleq1d	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to \left(x{+}_{K}y\in {\mathrm{Base}}_K\leftrightarrow x{+}_{L}y\in {\mathrm{Base}}_K\right)$$
17	16	2ralbidva	$$⊢\phi \to \left(\forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_{K}x{+}_{K}y\in {\mathrm{Base}}_K\leftrightarrow \forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_{K}x{+}_{L}y\in {\mathrm{Base}}_K\right)$$
18	1 2	eqtr3d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
19	18	eleq2d	$$⊢\phi \to \left(x{+}_{L}y\in {\mathrm{Base}}_K\leftrightarrow x{+}_{L}y\in {\mathrm{Base}}_L\right)$$
20	18 19	raleqbidv	$$⊢\phi \to \left(\forall y\in {\mathrm{Base}}_{K}x{+}_{L}y\in {\mathrm{Base}}_K\leftrightarrow \forall y\in {\mathrm{Base}}_{L}x{+}_{L}y\in {\mathrm{Base}}_L\right)$$
21	18 20	raleqbidv	$$⊢\phi \to \left(\forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_{K}x{+}_{L}y\in {\mathrm{Base}}_K\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}x{+}_{L}y\in {\mathrm{Base}}_L\right)$$
22	17 21	bitrd	$$⊢\phi \to \left(\forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_{K}x{+}_{K}y\in {\mathrm{Base}}_K\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}x{+}_{L}y\in {\mathrm{Base}}_L\right)$$
23		n0	$$⊢B\ne \varnothing \leftrightarrow \exists aa\in B$$
24	1	eleq2d	$$⊢\phi \to \left(a\in B\leftrightarrow a\in {\mathrm{Base}}_K\right)$$
25		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
26		eqid	$$⊢{+}_K={+}_K$$
27	25 26	ismgmn0	$$⊢a\in {\mathrm{Base}}_K\to \left(K\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_{K}x{+}_{K}y\in {\mathrm{Base}}_K\right)$$
28	24 27	syl6bi	$$⊢\phi \to \left(a\in B\to \left(K\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_{K}x{+}_{K}y\in {\mathrm{Base}}_K\right)\right)$$
29	28	exlimdv	$$⊢\phi \to \left(\exists aa\in B\to \left(K\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_{K}x{+}_{K}y\in {\mathrm{Base}}_K\right)\right)$$
30	23 29	syl5bi	$$⊢\phi \to \left(B\ne \varnothing \to \left(K\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_{K}x{+}_{K}y\in {\mathrm{Base}}_K\right)\right)$$
31	3 30	mpd	$$⊢\phi \to \left(K\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_{K}x{+}_{K}y\in {\mathrm{Base}}_K\right)$$
32	2	eleq2d	$$⊢\phi \to \left(a\in B\leftrightarrow a\in {\mathrm{Base}}_L\right)$$
33		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
34		eqid	$$⊢{+}_L={+}_L$$
35	33 34	ismgmn0	$$⊢a\in {\mathrm{Base}}_L\to \left(L\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}x{+}_{L}y\in {\mathrm{Base}}_L\right)$$
36	32 35	syl6bi	$$⊢\phi \to \left(a\in B\to \left(L\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}x{+}_{L}y\in {\mathrm{Base}}_L\right)\right)$$
37	36	exlimdv	$$⊢\phi \to \left(\exists aa\in B\to \left(L\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}x{+}_{L}y\in {\mathrm{Base}}_L\right)\right)$$
38	23 37	syl5bi	$$⊢\phi \to \left(B\ne \varnothing \to \left(L\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}x{+}_{L}y\in {\mathrm{Base}}_L\right)\right)$$
39	3 38	mpd	$$⊢\phi \to \left(L\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_L\forall y\in {\mathrm{Base}}_{L}x{+}_{L}y\in {\mathrm{Base}}_L\right)$$
40	22 31 39	3bitr4d	$$⊢\phi \to \left(K\in \mathrm{Mgm}\leftrightarrow L\in \mathrm{Mgm}\right)$$