Theorem lsmvalx

Description: Subspace sum value (for a group or vector space). Extended domain version of lsmval . (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	lsmvalx	$$⊢\left(G\in V\wedge T\subseteq B\wedge U\subseteq B\right)\to T\underset{\dot{}}{\oplus }U=\mathrm{ran}\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\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	1 2 3	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)$$
5	4	oveqd	$$⊢G\in V\to T\underset{\dot{}}{\oplus }U=T\left(t\in 𝒫B,u\in 𝒫B⟼\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)\right)U$$
6	1	fvexi	$$⊢B\in \mathrm{V}$$
7	6	elpw2	$$⊢T\in 𝒫B\leftrightarrow T\subseteq B$$
8	6	elpw2	$$⊢U\in 𝒫B\leftrightarrow U\subseteq B$$
9		mpoexga	$$⊢\left(T\in 𝒫B\wedge U\in 𝒫B\right)\to \left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)\in \mathrm{V}$$
10		rnexg	$$⊢\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)\in \mathrm{V}\to \mathrm{ran}\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)\in \mathrm{V}$$
11	9 10	syl	$$⊢\left(T\in 𝒫B\wedge U\in 𝒫B\right)\to \mathrm{ran}\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)\in \mathrm{V}$$
12		mpoeq12	$$⊢\left(t=T\wedge u=U\right)\to \left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)=\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)$$
13	12	rneqd	$$⊢\left(t=T\wedge u=U\right)\to \mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)=\mathrm{ran}\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)$$
14		eqid	$$⊢\left(t\in 𝒫B,u\in 𝒫B⟼\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}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)$$
15	13 14	ovmpoga	$$⊢\left(T\in 𝒫B\wedge U\in 𝒫B\wedge \mathrm{ran}\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)\in \mathrm{V}\right)\to T\left(t\in 𝒫B,u\in 𝒫B⟼\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)\right)U=\mathrm{ran}\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)$$
16	11 15	mpd3an3	$$⊢\left(T\in 𝒫B\wedge U\in 𝒫B\right)\to T\left(t\in 𝒫B,u\in 𝒫B⟼\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)\right)U=\mathrm{ran}\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)$$
17	7 8 16	syl2anbr	$$⊢\left(T\subseteq B\wedge U\subseteq B\right)\to T\left(t\in 𝒫B,u\in 𝒫B⟼\mathrm{ran}\left(x\in t,y\in u⟼x\underset{\dot{}}{+}y\right)\right)U=\mathrm{ran}\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)$$
18	5 17	sylan9eq	$$⊢\left(G\in V\wedge \left(T\subseteq B\wedge U\subseteq B\right)\right)\to T\underset{\dot{}}{\oplus }U=\mathrm{ran}\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)$$
19	18	3impb	$$⊢\left(G\in V\wedge T\subseteq B\wedge U\subseteq B\right)\to T\underset{\dot{}}{\oplus }U=\mathrm{ran}\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)$$