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

Proof

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