Metamath Proof Explorer


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 = Base G
grplsm0l.p ˙ = LSSum G
grplsm0l.0 0 ˙ = 0 G
Assertion grplsm0l G Grp A B A 0 ˙ ˙ A = A

Proof

Step Hyp Ref Expression
1 grplsm0l.b B = Base G
2 grplsm0l.p ˙ = LSSum G
3 grplsm0l.0 0 ˙ = 0 G
4 1 3 grpidcl G Grp 0 ˙ B
5 4 snssd G Grp 0 ˙ B
6 eqid + G = + G
7 1 6 2 lsmelvalx G Grp 0 ˙ B A B x 0 ˙ ˙ A o 0 ˙ a A x = o + G a
8 7 3expa G Grp 0 ˙ B A B x 0 ˙ ˙ A o 0 ˙ a A x = o + G a
9 8 an32s G Grp A B 0 ˙ B x 0 ˙ ˙ A o 0 ˙ a A x = o + G a
10 5 9 mpidan G Grp A B x 0 ˙ ˙ A o 0 ˙ a A x = o + G a
11 10 3adant3 G Grp A B A x 0 ˙ ˙ A o 0 ˙ a A x = o + G a
12 simpl1 G Grp A B A a A G Grp
13 simp2 G Grp A B A A B
14 13 sselda G Grp A B A a A a B
15 1 6 3 grplid G Grp a B 0 ˙ + G a = a
16 12 14 15 syl2anc G Grp A B A a A 0 ˙ + G a = a
17 16 eqeq2d G Grp A B A a A x = 0 ˙ + G a x = a
18 equcom x = a a = x
19 17 18 bitrdi G Grp A B A a A x = 0 ˙ + G a a = x
20 19 rexbidva G Grp A B A a A x = 0 ˙ + G a a A a = x
21 3 fvexi 0 ˙ V
22 oveq1 o = 0 ˙ o + G a = 0 ˙ + G a
23 22 eqeq2d o = 0 ˙ x = o + G a x = 0 ˙ + G a
24 23 rexbidv o = 0 ˙ a A x = o + G a a A x = 0 ˙ + G a
25 21 24 rexsn o 0 ˙ a A x = o + G a a A x = 0 ˙ + G a
26 risset x A a A a = x
27 20 25 26 3bitr4g G Grp A B A o 0 ˙ a A x = o + G a x A
28 11 27 bitrd G Grp A B A x 0 ˙ ˙ A x A
29 28 eqrdv G Grp A B A 0 ˙ ˙ A = A