Theorem lsmsnorb

Description: The sumset of a group with a single element is the element's orbit by the group action. See gaorb . (Contributed by Thierry Arnoux, 21-Jan-2024)

	Ref	Expression
Hypotheses	lsmsnorb.1	$$⊢B={\mathrm{Base}}_G$$
	lsmsnorb.2	$$⊢\underset{\dot{}}{+}={+}_G$$
	lsmsnorb.3	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
	lsmsnorb.4	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag\underset{\dot{}}{+}x=y\right)\right\}$$
	lsmsnorb.5	$$⊢\phi \to G\in \mathrm{Mnd}$$
	lsmsnorb.6	$$⊢\phi \to A\subseteq B$$
	lsmsnorb.7	$$⊢\phi \to X\in B$$
Assertion	lsmsnorb	$$⊢\phi \to A\underset{\dot{}}{\oplus }\left\{X\right\}=\left[X\right]\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		lsmsnorb.1	$$⊢B={\mathrm{Base}}_G$$
2		lsmsnorb.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		lsmsnorb.3	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
4		lsmsnorb.4	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag\underset{\dot{}}{+}x=y\right)\right\}$$
5		lsmsnorb.5	$$⊢\phi \to G\in \mathrm{Mnd}$$
6		lsmsnorb.6	$$⊢\phi \to A\subseteq B$$
7		lsmsnorb.7	$$⊢\phi \to X\in B$$
8	7	snssd	$$⊢\phi \to \left\{X\right\}\subseteq B$$
9	1 3	lsmssv	$$⊢\left(G\in \mathrm{Mnd}\wedge A\subseteq B\wedge \left\{X\right\}\subseteq B\right)\to A\underset{\dot{}}{\oplus }\left\{X\right\}\subseteq B$$
10	5 6 8 9	syl3anc	$$⊢\phi \to A\underset{\dot{}}{\oplus }\left\{X\right\}\subseteq B$$
11	10	sselda	$$⊢\left(\phi \wedge k\in \left(A\underset{\dot{}}{\oplus }\left\{X\right\}\right)\right)\to k\in B$$
12		df-ec	$$⊢\left[X\right]\underset{\dot{}}{\sim }=\underset{\dot{}}{\sim }\left[\left\{X\right\}\right]$$
13		imassrn	$$⊢\underset{\dot{}}{\sim }\left[\left\{X\right\}\right]\subseteq \mathrm{ran}\underset{\dot{}}{\sim }$$
14	4	rneqi	$$⊢\mathrm{ran}\underset{\dot{}}{\sim }=\mathrm{ran}\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag\underset{\dot{}}{+}x=y\right)\right\}$$
15		rnopab	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag\underset{\dot{}}{+}x=y\right)\right\}=\left\{y|\exists x\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag\underset{\dot{}}{+}x=y\right)\right\}$$
16		vex	$$⊢x\in \mathrm{V}$$
17		vex	$$⊢y\in \mathrm{V}$$
18	16 17	prss	$$⊢\left(x\in B\wedge y\in B\right)\leftrightarrow \left\{x,y\right\}\subseteq B$$
19	18	biimpri	$$⊢\left\{x,y\right\}\subseteq B\to \left(x\in B\wedge y\in B\right)$$
20	19	simprd	$$⊢\left\{x,y\right\}\subseteq B\to y\in B$$
21	20	adantr	$$⊢\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag\underset{\dot{}}{+}x=y\right)\to y\in B$$
22	21	exlimiv	$$⊢\exists x\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag\underset{\dot{}}{+}x=y\right)\to y\in B$$
23	22	abssi	$$⊢\left\{y|\exists x\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag\underset{\dot{}}{+}x=y\right)\right\}\subseteq B$$
24	15 23	eqsstri	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag\underset{\dot{}}{+}x=y\right)\right\}\subseteq B$$
25	14 24	eqsstri	$$⊢\mathrm{ran}\underset{\dot{}}{\sim }\subseteq B$$
26	13 25	sstri	$$⊢\underset{\dot{}}{\sim }\left[\left\{X\right\}\right]\subseteq B$$
27	26	a1i	$$⊢\phi \to \underset{\dot{}}{\sim }\left[\left\{X\right\}\right]\subseteq B$$
28	12 27	eqsstrid	$$⊢\phi \to \left[X\right]\underset{\dot{}}{\sim }\subseteq B$$
29	28	sselda	$$⊢\left(\phi \wedge k\in \left[X\right]\underset{\dot{}}{\sim }\right)\to k\in B$$
30	7	anim1i	$$⊢\left(\phi \wedge k\in B\right)\to \left(X\in B\wedge k\in B\right)$$
31	30	biantrurd	$$⊢\left(\phi \wedge k\in B\right)\to \left(\exists h\in Ah\underset{\dot{}}{+}X=k\leftrightarrow \left(\left(X\in B\wedge k\in B\right)\wedge \exists h\in Ah\underset{\dot{}}{+}X=k\right)\right)$$
32		df-3an	$$⊢\left(X\in B\wedge k\in B\wedge \exists h\in Ah\underset{\dot{}}{+}X=k\right)\leftrightarrow \left(\left(X\in B\wedge k\in B\right)\wedge \exists h\in Ah\underset{\dot{}}{+}X=k\right)$$
33	31 32	syl6bbr	$$⊢\left(\phi \wedge k\in B\right)\to \left(\exists h\in Ah\underset{\dot{}}{+}X=k\leftrightarrow \left(X\in B\wedge k\in B\wedge \exists h\in Ah\underset{\dot{}}{+}X=k\right)\right)$$
34	4	gaorb	$$⊢X\underset{\dot{}}{\sim }k\leftrightarrow \left(X\in B\wedge k\in B\wedge \exists h\in Ah\underset{\dot{}}{+}X=k\right)$$
35	33 34	syl6rbbr	$$⊢\left(\phi \wedge k\in B\right)\to \left(X\underset{\dot{}}{\sim }k\leftrightarrow \exists h\in Ah\underset{\dot{}}{+}X=k\right)$$
36		vex	$$⊢k\in \mathrm{V}$$
37	7	adantr	$$⊢\left(\phi \wedge k\in B\right)\to X\in B$$
38		elecg	$$⊢\left(k\in \mathrm{V}\wedge X\in B\right)\to \left(k\in \left[X\right]\underset{\dot{}}{\sim }\leftrightarrow X\underset{\dot{}}{\sim }k\right)$$
39	36 37 38	sylancr	$$⊢\left(\phi \wedge k\in B\right)\to \left(k\in \left[X\right]\underset{\dot{}}{\sim }\leftrightarrow X\underset{\dot{}}{\sim }k\right)$$
40	5	adantr	$$⊢\left(\phi \wedge k\in B\right)\to G\in \mathrm{Mnd}$$
41	6	adantr	$$⊢\left(\phi \wedge k\in B\right)\to A\subseteq B$$
42	1 2 3 40 41 37	elgrplsmsn	$$⊢\left(\phi \wedge k\in B\right)\to \left(k\in \left(A\underset{\dot{}}{\oplus }\left\{X\right\}\right)\leftrightarrow \exists h\in Ak=h\underset{\dot{}}{+}X\right)$$
43		eqcom	$$⊢k=h\underset{\dot{}}{+}X\leftrightarrow h\underset{\dot{}}{+}X=k$$
44	43	rexbii	$$⊢\exists h\in Ak=h\underset{\dot{}}{+}X\leftrightarrow \exists h\in Ah\underset{\dot{}}{+}X=k$$
45	42 44	syl6bb	$$⊢\left(\phi \wedge k\in B\right)\to \left(k\in \left(A\underset{\dot{}}{\oplus }\left\{X\right\}\right)\leftrightarrow \exists h\in Ah\underset{\dot{}}{+}X=k\right)$$
46	35 39 45	3bitr4rd	$$⊢\left(\phi \wedge k\in B\right)\to \left(k\in \left(A\underset{\dot{}}{\oplus }\left\{X\right\}\right)\leftrightarrow k\in \left[X\right]\underset{\dot{}}{\sim }\right)$$
47	11 29 46	eqrdav	$$⊢\phi \to A\underset{\dot{}}{\oplus }\left\{X\right\}=\left[X\right]\underset{\dot{}}{\sim }$$