Theorem gsummgmpropd

Description: A stronger version of gsumpropd if at least one of the involved structures is a magma, see gsumpropd2 . (Contributed by AV, 31-Jan-2020)

	Ref	Expression
Hypotheses	gsummgmpropd.f	$$⊢\phi \to F\in V$$
	gsummgmpropd.g	$$⊢\phi \to G\in W$$
	gsummgmpropd.h	$$⊢\phi \to H\in X$$
	gsummgmpropd.b	$$⊢\phi \to {\mathrm{Base}}_G={\mathrm{Base}}_H$$
	gsummgmpropd.m	$$⊢\phi \to G\in \mathrm{Mgm}$$
	gsummgmpropd.e	$$⊢\left(\phi \wedge \left(s\in {\mathrm{Base}}_G\wedge t\in {\mathrm{Base}}_G\right)\right)\to s{+}_{G}t=s{+}_{H}t$$
	gsummgmpropd.n	$$⊢\phi \to \mathrm{Fun}F$$
	gsummgmpropd.r	$$⊢\phi \to \mathrm{ran}F\subseteq {\mathrm{Base}}_G$$
Assertion	gsummgmpropd	$$⊢\phi \to {\sum }_{G}F={\sum }_{H}F$$

Proof

Step	Hyp	Ref	Expression
1		gsummgmpropd.f	$$⊢\phi \to F\in V$$
2		gsummgmpropd.g	$$⊢\phi \to G\in W$$
3		gsummgmpropd.h	$$⊢\phi \to H\in X$$
4		gsummgmpropd.b	$$⊢\phi \to {\mathrm{Base}}_G={\mathrm{Base}}_H$$
5		gsummgmpropd.m	$$⊢\phi \to G\in \mathrm{Mgm}$$
6		gsummgmpropd.e	$$⊢\left(\phi \wedge \left(s\in {\mathrm{Base}}_G\wedge t\in {\mathrm{Base}}_G\right)\right)\to s{+}_{G}t=s{+}_{H}t$$
7		gsummgmpropd.n	$$⊢\phi \to \mathrm{Fun}F$$
8		gsummgmpropd.r	$$⊢\phi \to \mathrm{ran}F\subseteq {\mathrm{Base}}_G$$
9		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
10		eqid	$$⊢{+}_G={+}_G$$
11	9 10	mgmcl	$$⊢\left(G\in \mathrm{Mgm}\wedge s\in {\mathrm{Base}}_G\wedge t\in {\mathrm{Base}}_G\right)\to s{+}_{G}t\in {\mathrm{Base}}_G$$
12	11	3expib	$$⊢G\in \mathrm{Mgm}\to \left(\left(s\in {\mathrm{Base}}_G\wedge t\in {\mathrm{Base}}_G\right)\to s{+}_{G}t\in {\mathrm{Base}}_G\right)$$
13	5 12	syl	$$⊢\phi \to \left(\left(s\in {\mathrm{Base}}_G\wedge t\in {\mathrm{Base}}_G\right)\to s{+}_{G}t\in {\mathrm{Base}}_G\right)$$
14	13	imp	$$⊢\left(\phi \wedge \left(s\in {\mathrm{Base}}_G\wedge t\in {\mathrm{Base}}_G\right)\right)\to s{+}_{G}t\in {\mathrm{Base}}_G$$
15	1 2 3 4 14 6 7 8	gsumpropd2	$$⊢\phi \to {\sum }_{G}F={\sum }_{H}F$$