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 ` G )
lsmsnorb2.3 
|- .(+) = ( LSSum ` G )
lsmsnorb2.4 
|- .~ = { <. x , y >. | ( { x , y } C_ B /\ E. g e. A ( x .+ g ) = y ) }
lsmsnorb2.5 
|- ( ph -> G e. Mnd )
lsmsnorb2.6 
|- ( ph -> A C_ B )
lsmsnorb2.7 
|- ( ph -> X e. B )
Assertion lsmsnorb2 
|- ( ph -> ( { X } .(+) A ) = [ X ] .~ )

Proof

Step Hyp Ref Expression
1 lsmsnorb2.1 
 |-  B = ( Base ` G )
2 lsmsnorb2.2 
 |-  .+ = ( +g ` G )
3 lsmsnorb2.3 
 |-  .(+) = ( LSSum ` G )
4 lsmsnorb2.4 
 |-  .~ = { <. x , y >. | ( { x , y } C_ B /\ E. g e. A ( x .+ g ) = y ) }
5 lsmsnorb2.5 
 |-  ( ph -> G e. Mnd )
6 lsmsnorb2.6 
 |-  ( ph -> A C_ B )
7 lsmsnorb2.7 
 |-  ( ph -> X e. B )
8 eqid 
 |-  ( oppG ` G ) = ( oppG ` G )
9 8 3 oppglsm 
 |-  ( A ( LSSum ` ( oppG ` G ) ) { X } ) = ( { X } .(+) A )
10 8 1 oppgbas 
 |-  B = ( Base ` ( oppG ` G ) )
11 eqid 
 |-  ( +g ` ( oppG ` G ) ) = ( +g ` ( oppG ` G ) )
12 eqid 
 |-  ( LSSum ` ( oppG ` G ) ) = ( LSSum ` ( oppG ` G ) )
13 2 8 11 oppgplus 
 |-  ( g ( +g ` ( oppG ` G ) ) x ) = ( x .+ g )
14 13 eqeq1i 
 |-  ( ( g ( +g ` ( oppG ` G ) ) x ) = y <-> ( x .+ g ) = y )
15 14 rexbii 
 |-  ( E. g e. A ( g ( +g ` ( oppG ` G ) ) x ) = y <-> E. g e. A ( x .+ g ) = y )
16 15 anbi2i 
 |-  ( ( { x , y } C_ B /\ E. g e. A ( g ( +g ` ( oppG ` G ) ) x ) = y ) <-> ( { x , y } C_ B /\ E. g e. A ( x .+ g ) = y ) )
17 16 opabbii 
 |-  { <. x , y >. | ( { x , y } C_ B /\ E. g e. A ( g ( +g ` ( oppG ` G ) ) x ) = y ) } = { <. x , y >. | ( { x , y } C_ B /\ E. g e. A ( x .+ g ) = y ) }
18 4 17 eqtr4i 
 |-  .~ = { <. x , y >. | ( { x , y } C_ B /\ E. g e. A ( g ( +g ` ( oppG ` G ) ) x ) = y ) }
19 8 oppgmnd 
 |-  ( G e. Mnd -> ( oppG ` G ) e. Mnd )
20 5 19 syl 
 |-  ( ph -> ( oppG ` G ) e. Mnd )
21 10 11 12 18 20 6 7 lsmsnorb 
 |-  ( ph -> ( A ( LSSum ` ( oppG ` G ) ) { X } ) = [ X ] .~ )
22 9 21 eqtr3id 
 |-  ( ph -> ( { X } .(+) A ) = [ X ] .~ )