Theorem lsmval

Description: Subgroup sum value (for a left module or left vector space). (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	lsmval.v	$$⊢B={\mathrm{Base}}_G$$
	lsmval.a	$$⊢\underset{\dot{}}{+}={+}_G$$
	lsmval.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
Assertion	lsmval	$$⊢\left(T\in \mathrm{SubGrp}\left(G\right)\wedge U\in \mathrm{SubGrp}\left(G\right)\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		lsmval.v	$$⊢B={\mathrm{Base}}_G$$
2		lsmval.a	$$⊢\underset{\dot{}}{+}={+}_G$$
3		lsmval.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
4		subgrcl	$$⊢T\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$
5	1	subgss	$$⊢T\in \mathrm{SubGrp}\left(G\right)\to T\subseteq B$$
6	1	subgss	$$⊢U\in \mathrm{SubGrp}\left(G\right)\to U\subseteq B$$
7	1 2 3	lsmvalx	$$⊢\left(G\in \mathrm{Grp}\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)$$
8	4 5 6 7	syl2an3an	$$⊢\left(T\in \mathrm{SubGrp}\left(G\right)\wedge U\in \mathrm{SubGrp}\left(G\right)\right)\to T\underset{\dot{}}{\oplus }U=\mathrm{ran}\left(x\in T,y\in U⟼x\underset{\dot{}}{+}y\right)$$