Theorem lsmsnorb2

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

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

Proof

Step	Hyp	Ref	Expression
1		lsmsnorb2.1	$$⊢B={\mathrm{Base}}_G$$
2		lsmsnorb2.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		lsmsnorb2.3	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
4		lsmsnorb2.4	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ax\underset{\dot{}}{+}g=y\right)\right\}$$
5		lsmsnorb2.5	$$⊢\phi \to G\in \mathrm{Mnd}$$
6		lsmsnorb2.6	$$⊢\phi \to A\subseteq B$$
7		lsmsnorb2.7	$$⊢\phi \to X\in B$$
8		eqid	$$⊢{opp}_{𝑔}\left(G\right)={opp}_{𝑔}\left(G\right)$$
9	8 3	oppglsm	$$⊢A\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)\left\{X\right\}=\left\{X\right\}\underset{\dot{}}{\oplus }A$$
10	8 1	oppgbas	$$⊢B={\mathrm{Base}}_{{opp}_{𝑔}\left(G\right)}$$
11		eqid	$$⊢{+}_{{opp}_{𝑔}\left(G\right)}={+}_{{opp}_{𝑔}\left(G\right)}$$
12		eqid	$$⊢\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)=\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)$$
13	2 8 11	oppgplus	$$⊢g{+}_{{opp}_{𝑔}\left(G\right)}x=x\underset{\dot{}}{+}g$$
14	13	eqeq1i	$$⊢g{+}_{{opp}_{𝑔}\left(G\right)}x=y\leftrightarrow x\underset{\dot{}}{+}g=y$$
15	14	rexbii	$$⊢\exists g\in Ag{+}_{{opp}_{𝑔}\left(G\right)}x=y\leftrightarrow \exists g\in Ax\underset{\dot{}}{+}g=y$$
16	15	anbi2i	$$⊢\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag{+}_{{opp}_{𝑔}\left(G\right)}x=y\right)\leftrightarrow \left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ax\underset{\dot{}}{+}g=y\right)$$
17	16	opabbii	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag{+}_{{opp}_{𝑔}\left(G\right)}x=y\right)\right\}=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ax\underset{\dot{}}{+}g=y\right)\right\}$$
18	4 17	eqtr4i	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq B\wedge \exists g\in Ag{+}_{{opp}_{𝑔}\left(G\right)}x=y\right)\right\}$$
19	8	oppgmnd	$$⊢G\in \mathrm{Mnd}\to {opp}_{𝑔}\left(G\right)\in \mathrm{Mnd}$$
20	5 19	syl	$$⊢\phi \to {opp}_{𝑔}\left(G\right)\in \mathrm{Mnd}$$
21	10 11 12 18 20 6 7	lsmsnorb	$$⊢\phi \to A\mathrm{LSSum}\left({opp}_{𝑔}\left(G\right)\right)\left\{X\right\}=\left[X\right]\underset{\dot{}}{\sim }$$
22	9 21	eqtr3id	$$⊢\phi \to \left\{X\right\}\underset{\dot{}}{\oplus }A=\left[X\right]\underset{\dot{}}{\sim }$$