Theorem lsmfval

Description: The subgroup sum function (for a group or vector space). (Contributed by NM, 28-Jan-2014) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	lsmfval.v	$$⊢B={\mathrm{Base}}_G$$
	lsmfval.a	$$⊢\underset{\dot{}}{+}={+}_G$$
	lsmfval.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
Assertion	lsmfval	$$⊢G\in V\to \underset{\dot{}}{\oplus }=\left(t\in 𝒫B,u\in 𝒫B⟼\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsmfval.v	$$⊢B={\mathrm{Base}}_G$$
2		lsmfval.a	$$⊢\underset{\dot{}}{+}={+}_G$$
3		lsmfval.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
4		elex	$$⊢G\in V\to G\in \mathrm{V}$$
5		fveq2	$$⊢w=G\to {\mathrm{Base}}_w={\mathrm{Base}}_G$$
6	5 1	syl6eqr	$$⊢w=G\to {\mathrm{Base}}_w=B$$
7	6	pweqd	$$⊢w=G\to 𝒫{\mathrm{Base}}_w=𝒫B$$
8		fveq2	$$⊢w=G\to {+}_w={+}_G$$
9	8 2	syl6eqr	$$⊢w=G\to {+}_w=\underset{\dot{}}{+}$$
10	9	oveqd	$$⊢w=G\to x{+}_{w}y=x\underset{\dot{}}{+}y$$
11	10	mpoeq3dv	$$⊢w=G\to \left(x\in t,y\in u⟼x{+}_{w}y\right)=\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)$$
12	11	rneqd	$$⊢w=G\to \mathrm{ran}\left(x\in t,y\in u⟼x{+}_{w}y\right)=\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)$$
13	7 7 12	mpoeq123dv	$$⊢w=G\to \left(t\in 𝒫{\mathrm{Base}}_w,u\in 𝒫{\mathrm{Base}}_w⟼\mathrm{ran}\left(x\in t,y\in u⟼x{+}_{w}y\right)\right)=\left(t\in 𝒫B,u\in 𝒫B⟼\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)\right)$$
14		df-lsm	$$⊢\mathrm{LSSum}=\left(w\in \mathrm{V}⟼\left(t\in 𝒫{\mathrm{Base}}_w,u\in 𝒫{\mathrm{Base}}_w⟼\mathrm{ran}\left(x\in t,y\in u⟼x{+}_{w}y\right)\right)\right)$$
15	1	fvexi	$$⊢B\in \mathrm{V}$$
16	15	pwex	$$⊢𝒫B\in \mathrm{V}$$
17	16 16	mpoex	$$⊢\left(t\in 𝒫B,u\in 𝒫B⟼\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)\right)\in \mathrm{V}$$
18	13 14 17	fvmpt	$$⊢G\in \mathrm{V}\to \mathrm{LSSum}\left(G\right)=\left(t\in 𝒫B,u\in 𝒫B⟼\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)\right)$$
19	4 18	syl	$$⊢G\in V\to \mathrm{LSSum}\left(G\right)=\left(t\in 𝒫B,u\in 𝒫B⟼\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)\right)$$
20	3 19	syl5eq	$$⊢G\in V\to \underset{\dot{}}{\oplus }=\left(t\in 𝒫B,u\in 𝒫B⟼\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)\right)$$