Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 lsmsnorb2.1 B = Base G
2 lsmsnorb2.2 + ˙ = + G
3 lsmsnorb2.3 ˙ = LSSum G
4 lsmsnorb2.4 ˙ = x y | x y B g A x + ˙ g = y
5 lsmsnorb2.5 φ G Mnd
6 lsmsnorb2.6 φ A B
7 lsmsnorb2.7 φ X B
8 eqid opp 𝑔 G = opp 𝑔 G
9 8 3 oppglsm A LSSum opp 𝑔 G X = X ˙ A
10 8 1 oppgbas B = Base opp 𝑔 G
11 eqid + opp 𝑔 G = + opp 𝑔 G
12 eqid LSSum opp 𝑔 G = LSSum opp 𝑔 G
13 2 8 11 oppgplus g + opp 𝑔 G x = x + ˙ g
14 13 eqeq1i g + opp 𝑔 G x = y x + ˙ g = y
15 14 rexbii g A g + opp 𝑔 G x = y g A x + ˙ g = y
16 15 anbi2i x y B g A g + opp 𝑔 G x = y x y B g A x + ˙ g = y
17 16 opabbii x y | x y B g A g + opp 𝑔 G x = y = x y | x y B g A x + ˙ g = y
18 4 17 eqtr4i ˙ = x y | x y B g A g + opp 𝑔 G x = y
19 8 oppgmnd G Mnd opp 𝑔 G Mnd
20 5 19 syl φ opp 𝑔 G Mnd
21 10 11 12 18 20 6 7 lsmsnorb φ A LSSum opp 𝑔 G X = X ˙
22 9 21 eqtr3id φ X ˙ A = X ˙