Theorem grplsm0l

Description: Sumset with the identity singleton is the original set. (Contributed by Thierry Arnoux, 27-Jul-2024)

	Ref	Expression
Hypotheses	grplsm0l.b	$$⊢B={\mathrm{Base}}_G$$
	grplsm0l.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
	grplsm0l.0	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	grplsm0l	$$⊢\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\to \left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\oplus }A=A$$

Proof

Step	Hyp	Ref	Expression
1		grplsm0l.b	$$⊢B={\mathrm{Base}}_G$$
2		grplsm0l.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
3		grplsm0l.0	$$⊢\underset{\dot{}}{0}=0_G$$
4	1 3	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in B$$
5	4	snssd	$$⊢G\in \mathrm{Grp}\to \left\{\underset{\dot{}}{0}\right\}\subseteq B$$
6		eqid	$$⊢{+}_G={+}_G$$
7	1 6 2	lsmelvalx	$$⊢\left(G\in \mathrm{Grp}\wedge \left\{\underset{\dot{}}{0}\right\}\subseteq B\wedge A\subseteq B\right)\to \left(x\in \left(\left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\oplus }A\right)\leftrightarrow \exists o\in \left\{\underset{\dot{}}{0}\right\}\exists a\in Ax=o{+}_{G}a\right)$$
8	7	3expa	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left\{\underset{\dot{}}{0}\right\}\subseteq B\right)\wedge A\subseteq B\right)\to \left(x\in \left(\left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\oplus }A\right)\leftrightarrow \exists o\in \left\{\underset{\dot{}}{0}\right\}\exists a\in Ax=o{+}_{G}a\right)$$
9	8	an32s	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\subseteq B\right)\wedge \left\{\underset{\dot{}}{0}\right\}\subseteq B\right)\to \left(x\in \left(\left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\oplus }A\right)\leftrightarrow \exists o\in \left\{\underset{\dot{}}{0}\right\}\exists a\in Ax=o{+}_{G}a\right)$$
10	5 9	mpidan	$$⊢\left(G\in \mathrm{Grp}\wedge A\subseteq B\right)\to \left(x\in \left(\left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\oplus }A\right)\leftrightarrow \exists o\in \left\{\underset{\dot{}}{0}\right\}\exists a\in Ax=o{+}_{G}a\right)$$
11	10	3adant3	$$⊢\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\to \left(x\in \left(\left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\oplus }A\right)\leftrightarrow \exists o\in \left\{\underset{\dot{}}{0}\right\}\exists a\in Ax=o{+}_{G}a\right)$$
12		simpl1	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\wedge a\in A\right)\to G\in \mathrm{Grp}$$
13		simp2	$$⊢\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\to A\subseteq B$$
14	13	sselda	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\wedge a\in A\right)\to a\in B$$
15	1 6 3	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge a\in B\right)\to \underset{\dot{}}{0}{+}_{G}a=a$$
16	12 14 15	syl2anc	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\wedge a\in A\right)\to \underset{\dot{}}{0}{+}_{G}a=a$$
17	16	eqeq2d	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\wedge a\in A\right)\to \left(x=\underset{\dot{}}{0}{+}_{G}a\leftrightarrow x=a\right)$$
18		equcom	$$⊢x=a\leftrightarrow a=x$$
19	17 18	bitrdi	$$⊢\left(\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\wedge a\in A\right)\to \left(x=\underset{\dot{}}{0}{+}_{G}a\leftrightarrow a=x\right)$$
20	19	rexbidva	$$⊢\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\to \left(\exists a\in Ax=\underset{\dot{}}{0}{+}_{G}a\leftrightarrow \exists a\in Aa=x\right)$$
21	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
22		oveq1	$$⊢o=\underset{\dot{}}{0}\to o{+}_{G}a=\underset{\dot{}}{0}{+}_{G}a$$
23	22	eqeq2d	$$⊢o=\underset{\dot{}}{0}\to \left(x=o{+}_{G}a\leftrightarrow x=\underset{\dot{}}{0}{+}_{G}a\right)$$
24	23	rexbidv	$$⊢o=\underset{\dot{}}{0}\to \left(\exists a\in Ax=o{+}_{G}a\leftrightarrow \exists a\in Ax=\underset{\dot{}}{0}{+}_{G}a\right)$$
25	21 24	rexsn	$$⊢\exists o\in \left\{\underset{\dot{}}{0}\right\}\exists a\in Ax=o{+}_{G}a\leftrightarrow \exists a\in Ax=\underset{\dot{}}{0}{+}_{G}a$$
26		risset	$$⊢x\in A\leftrightarrow \exists a\in Aa=x$$
27	20 25 26	3bitr4g	$$⊢\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\to \left(\exists o\in \left\{\underset{\dot{}}{0}\right\}\exists a\in Ax=o{+}_{G}a\leftrightarrow x\in A\right)$$
28	11 27	bitrd	$$⊢\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\to \left(x\in \left(\left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\oplus }A\right)\leftrightarrow x\in A\right)$$
29	28	eqrdv	$$⊢\left(G\in \mathrm{Grp}\wedge A\subseteq B\wedge A\ne \varnothing \right)\to \left\{\underset{\dot{}}{0}\right\}\underset{\dot{}}{\oplus }A=A$$