Theorem gsumzresunsn

Description: Append an element to a finite group sum expressed as a function restriction. (Contributed by Thierry Arnoux, 20-Nov-2023)

	Ref	Expression
Hypotheses	gsumzresunsn.b	$$⊢B={\mathrm{Base}}_G$$
	gsumzresunsn.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumzresunsn.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	gsumzresunsn.y	$$⊢Y=F\left(X\right)$$
	gsumzresunsn.f	$$⊢\phi \to F:C⟶B$$
	gsumzresunsn.1	$$⊢\phi \to A\subseteq C$$
	gsumzresunsn.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	gsumzresunsn.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	gsumzresunsn.2	$$⊢\phi \to \neg X\in A$$
	gsumzresunsn.3	$$⊢\phi \to X\in C$$
	gsumzresunsn.4	$$⊢\phi \to Y\in B$$
	gsumzresunsn.5	$$⊢\phi \to F\left[A\cup \left\{X\right\}\right]\subseteq Z\left(F\left[A\cup \left\{X\right\}\right]\right)$$
Assertion	gsumzresunsn	$$⊢\phi \to {\sum }_G\left({F\upharpoonright }_{\left(A\cup \left\{X\right\}\right)}\right)=\left({\sum }_G,\left({F\upharpoonright }_A\right)\right)\underset{\dot{}}{+}Y$$

Proof

Step	Hyp	Ref	Expression
1		gsumzresunsn.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumzresunsn.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsumzresunsn.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
4		gsumzresunsn.y	$$⊢Y=F\left(X\right)$$
5		gsumzresunsn.f	$$⊢\phi \to F:C⟶B$$
6		gsumzresunsn.1	$$⊢\phi \to A\subseteq C$$
7		gsumzresunsn.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
8		gsumzresunsn.a	$$⊢\phi \to A\in \mathrm{Fin}$$
9		gsumzresunsn.2	$$⊢\phi \to \neg X\in A$$
10		gsumzresunsn.3	$$⊢\phi \to X\in C$$
11		gsumzresunsn.4	$$⊢\phi \to Y\in B$$
12		gsumzresunsn.5	$$⊢\phi \to F\left[A\cup \left\{X\right\}\right]\subseteq Z\left(F\left[A\cup \left\{X\right\}\right]\right)$$
13		eqid	$$⊢\left(x\in \left(A\cup \left\{X\right\}\right)⟼F\left(x\right)\right)=\left(x\in \left(A\cup \left\{X\right\}\right)⟼F\left(x\right)\right)$$
14		df-ima	$$⊢F\left[A\cup \left\{X\right\}\right]=\mathrm{ran}\left({F\upharpoonright }_{\left(A\cup \left\{X\right\}\right)}\right)$$
15	10	snssd	$$⊢\phi \to \left\{X\right\}\subseteq C$$
16	6 15	unssd	$$⊢\phi \to A\cup \left\{X\right\}\subseteq C$$
17	5 16	feqresmpt	$$⊢\phi \to {F\upharpoonright }_{\left(A\cup \left\{X\right\}\right)}=\left(x\in \left(A\cup \left\{X\right\}\right)⟼F\left(x\right)\right)$$
18	17	rneqd	$$⊢\phi \to \mathrm{ran}\left({F\upharpoonright }_{\left(A\cup \left\{X\right\}\right)}\right)=\mathrm{ran}\left(x\in \left(A\cup \left\{X\right\}\right)⟼F\left(x\right)\right)$$
19	14 18	eqtrid	$$⊢\phi \to F\left[A\cup \left\{X\right\}\right]=\mathrm{ran}\left(x\in \left(A\cup \left\{X\right\}\right)⟼F\left(x\right)\right)$$
20	19	fveq2d	$$⊢\phi \to Z\left(F\left[A\cup \left\{X\right\}\right]\right)=Z\left(\mathrm{ran}\left(x\in \left(A\cup \left\{X\right\}\right)⟼F\left(x\right)\right)\right)$$
21	12 19 20	3sstr3d	$$⊢\phi \to \mathrm{ran}\left(x\in \left(A\cup \left\{X\right\}\right)⟼F\left(x\right)\right)\subseteq Z\left(\mathrm{ran}\left(x\in \left(A\cup \left\{X\right\}\right)⟼F\left(x\right)\right)\right)$$
22	5	adantr	$$⊢\left(\phi \wedge x\in A\right)\to F:C⟶B$$
23	6	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in C$$
24	22 23	ffvelrnd	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in B$$
25		simpr	$$⊢\left(\phi \wedge x=X\right)\to x=X$$
26	25	fveq2d	$$⊢\left(\phi \wedge x=X\right)\to F\left(x\right)=F\left(X\right)$$
27	26 4	eqtr4di	$$⊢\left(\phi \wedge x=X\right)\to F\left(x\right)=Y$$
28	1 2 3 13 7 8 21 24 10 9 11 27	gsumzunsnd	$$⊢\phi \to \underset{x\in A\cup \left\{X\right\}}{{\sum }_G}F\left(x\right)=\left(\underset{x\in A}{{\sum }_G},F\left(x\right)\right)\underset{\dot{}}{+}Y$$
29	17	oveq2d	$$⊢\phi \to {\sum }_G\left({F\upharpoonright }_{\left(A\cup \left\{X\right\}\right)}\right)=\underset{x\in A\cup \left\{X\right\}}{{\sum }_G}F\left(x\right)$$
30	5 6	feqresmpt	$$⊢\phi \to {F\upharpoonright }_A=\left(x\in A⟼F\left(x\right)\right)$$
31	30	oveq2d	$$⊢\phi \to {\sum }_G\left({F\upharpoonright }_A\right)=\underset{x\in A}{{\sum }_G}F\left(x\right)$$
32	31	oveq1d	$$⊢\phi \to \left({\sum }_G,\left({F\upharpoonright }_A\right)\right)\underset{\dot{}}{+}Y=\left(\underset{x\in A}{{\sum }_G},F\left(x\right)\right)\underset{\dot{}}{+}Y$$
33	28 29 32	3eqtr4d	$$⊢\phi \to {\sum }_G\left({F\upharpoonright }_{\left(A\cup \left\{X\right\}\right)}\right)=\left({\sum }_G,\left({F\upharpoonright }_A\right)\right)\underset{\dot{}}{+}Y$$