Metamath Proof Explorer


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 = Base G
lsmsnorb.2 + ˙ = + G
lsmsnorb.3 ˙ = LSSum G
lsmsnorb.4 ˙ = x y | x y B g A g + ˙ x = y
lsmsnorb.5 φ G Mnd
lsmsnorb.6 φ A B
lsmsnorb.7 φ X B
Assertion lsmsnorb φ A ˙ X = X ˙

Proof

Step Hyp Ref Expression
1 lsmsnorb.1 B = Base G
2 lsmsnorb.2 + ˙ = + G
3 lsmsnorb.3 ˙ = LSSum G
4 lsmsnorb.4 ˙ = x y | x y B g A g + ˙ x = y
5 lsmsnorb.5 φ G Mnd
6 lsmsnorb.6 φ A B
7 lsmsnorb.7 φ X B
8 7 snssd φ X B
9 1 3 lsmssv G Mnd A B X B A ˙ X B
10 5 6 8 9 syl3anc φ A ˙ X B
11 10 sselda φ k A ˙ X k B
12 df-ec X ˙ = ˙ X
13 imassrn ˙ X ran ˙
14 4 rneqi ran ˙ = ran x y | x y B g A g + ˙ x = y
15 rnopab ran x y | x y B g A g + ˙ x = y = y | x x y B g A g + ˙ x = y
16 vex x V
17 vex y V
18 16 17 prss x B y B x y B
19 18 biimpri x y B x B y B
20 19 simprd x y B y B
21 20 adantr x y B g A g + ˙ x = y y B
22 21 exlimiv x x y B g A g + ˙ x = y y B
23 22 abssi y | x x y B g A g + ˙ x = y B
24 15 23 eqsstri ran x y | x y B g A g + ˙ x = y B
25 14 24 eqsstri ran ˙ B
26 13 25 sstri ˙ X B
27 26 a1i φ ˙ X B
28 12 27 eqsstrid φ X ˙ B
29 28 sselda φ k X ˙ k B
30 4 gaorb X ˙ k X B k B h A h + ˙ X = k
31 7 anim1i φ k B X B k B
32 31 biantrurd φ k B h A h + ˙ X = k X B k B h A h + ˙ X = k
33 df-3an X B k B h A h + ˙ X = k X B k B h A h + ˙ X = k
34 32 33 bitr4di φ k B h A h + ˙ X = k X B k B h A h + ˙ X = k
35 30 34 bitr4id φ k B X ˙ k h A h + ˙ X = k
36 vex k V
37 7 adantr φ k B X B
38 elecg k V X B k X ˙ X ˙ k
39 36 37 38 sylancr φ k B k X ˙ X ˙ k
40 5 adantr φ k B G Mnd
41 6 adantr φ k B A B
42 1 2 3 40 41 37 elgrplsmsn φ k B k A ˙ X h A k = h + ˙ X
43 eqcom k = h + ˙ X h + ˙ X = k
44 43 rexbii h A k = h + ˙ X h A h + ˙ X = k
45 42 44 bitrdi φ k B k A ˙ X h A h + ˙ X = k
46 35 39 45 3bitr4rd φ k B k A ˙ X k X ˙
47 11 29 46 eqrdav φ A ˙ X = X ˙