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 𝐵 = ( Base ‘ 𝐺 )
lsmsnorb.2 + = ( +g𝐺 )
lsmsnorb.3 = ( LSSum ‘ 𝐺 )
lsmsnorb.4 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) }
lsmsnorb.5 ( 𝜑𝐺 ∈ Mnd )
lsmsnorb.6 ( 𝜑𝐴𝐵 )
lsmsnorb.7 ( 𝜑𝑋𝐵 )
Assertion lsmsnorb ( 𝜑 → ( 𝐴 { 𝑋 } ) = [ 𝑋 ] )

Proof

Step Hyp Ref Expression
1 lsmsnorb.1 𝐵 = ( Base ‘ 𝐺 )
2 lsmsnorb.2 + = ( +g𝐺 )
3 lsmsnorb.3 = ( LSSum ‘ 𝐺 )
4 lsmsnorb.4 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) }
5 lsmsnorb.5 ( 𝜑𝐺 ∈ Mnd )
6 lsmsnorb.6 ( 𝜑𝐴𝐵 )
7 lsmsnorb.7 ( 𝜑𝑋𝐵 )
8 7 snssd ( 𝜑 → { 𝑋 } ⊆ 𝐵 )
9 1 3 lsmssv ( ( 𝐺 ∈ Mnd ∧ 𝐴𝐵 ∧ { 𝑋 } ⊆ 𝐵 ) → ( 𝐴 { 𝑋 } ) ⊆ 𝐵 )
10 5 6 8 9 syl3anc ( 𝜑 → ( 𝐴 { 𝑋 } ) ⊆ 𝐵 )
11 10 sselda ( ( 𝜑𝑘 ∈ ( 𝐴 { 𝑋 } ) ) → 𝑘𝐵 )
12 df-ec [ 𝑋 ] = ( “ { 𝑋 } )
13 imassrn ( “ { 𝑋 } ) ⊆ ran
14 4 rneqi ran = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) }
15 rnopab ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) } = { 𝑦 ∣ ∃ 𝑥 ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) }
16 vex 𝑥 ∈ V
17 vex 𝑦 ∈ V
18 16 17 prss ( ( 𝑥𝐵𝑦𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 )
19 18 biimpri ( { 𝑥 , 𝑦 } ⊆ 𝐵 → ( 𝑥𝐵𝑦𝐵 ) )
20 19 simprd ( { 𝑥 , 𝑦 } ⊆ 𝐵𝑦𝐵 )
21 20 adantr ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) → 𝑦𝐵 )
22 21 exlimiv ( ∃ 𝑥 ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) → 𝑦𝐵 )
23 22 abssi { 𝑦 ∣ ∃ 𝑥 ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) } ⊆ 𝐵
24 15 23 eqsstri ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) } ⊆ 𝐵
25 14 24 eqsstri ran 𝐵
26 13 25 sstri ( “ { 𝑋 } ) ⊆ 𝐵
27 26 a1i ( 𝜑 → ( “ { 𝑋 } ) ⊆ 𝐵 )
28 12 27 eqsstrid ( 𝜑 → [ 𝑋 ] 𝐵 )
29 28 sselda ( ( 𝜑𝑘 ∈ [ 𝑋 ] ) → 𝑘𝐵 )
30 4 gaorb ( 𝑋 𝑘 ↔ ( 𝑋𝐵𝑘𝐵 ∧ ∃ 𝐴 ( + 𝑋 ) = 𝑘 ) )
31 7 anim1i ( ( 𝜑𝑘𝐵 ) → ( 𝑋𝐵𝑘𝐵 ) )
32 31 biantrurd ( ( 𝜑𝑘𝐵 ) → ( ∃ 𝐴 ( + 𝑋 ) = 𝑘 ↔ ( ( 𝑋𝐵𝑘𝐵 ) ∧ ∃ 𝐴 ( + 𝑋 ) = 𝑘 ) ) )
33 df-3an ( ( 𝑋𝐵𝑘𝐵 ∧ ∃ 𝐴 ( + 𝑋 ) = 𝑘 ) ↔ ( ( 𝑋𝐵𝑘𝐵 ) ∧ ∃ 𝐴 ( + 𝑋 ) = 𝑘 ) )
34 32 33 bitr4di ( ( 𝜑𝑘𝐵 ) → ( ∃ 𝐴 ( + 𝑋 ) = 𝑘 ↔ ( 𝑋𝐵𝑘𝐵 ∧ ∃ 𝐴 ( + 𝑋 ) = 𝑘 ) ) )
35 30 34 bitr4id ( ( 𝜑𝑘𝐵 ) → ( 𝑋 𝑘 ↔ ∃ 𝐴 ( + 𝑋 ) = 𝑘 ) )
36 vex 𝑘 ∈ V
37 7 adantr ( ( 𝜑𝑘𝐵 ) → 𝑋𝐵 )
38 elecg ( ( 𝑘 ∈ V ∧ 𝑋𝐵 ) → ( 𝑘 ∈ [ 𝑋 ] 𝑋 𝑘 ) )
39 36 37 38 sylancr ( ( 𝜑𝑘𝐵 ) → ( 𝑘 ∈ [ 𝑋 ] 𝑋 𝑘 ) )
40 5 adantr ( ( 𝜑𝑘𝐵 ) → 𝐺 ∈ Mnd )
41 6 adantr ( ( 𝜑𝑘𝐵 ) → 𝐴𝐵 )
42 1 2 3 40 41 37 elgrplsmsn ( ( 𝜑𝑘𝐵 ) → ( 𝑘 ∈ ( 𝐴 { 𝑋 } ) ↔ ∃ 𝐴 𝑘 = ( + 𝑋 ) ) )
43 eqcom ( 𝑘 = ( + 𝑋 ) ↔ ( + 𝑋 ) = 𝑘 )
44 43 rexbii ( ∃ 𝐴 𝑘 = ( + 𝑋 ) ↔ ∃ 𝐴 ( + 𝑋 ) = 𝑘 )
45 42 44 bitrdi ( ( 𝜑𝑘𝐵 ) → ( 𝑘 ∈ ( 𝐴 { 𝑋 } ) ↔ ∃ 𝐴 ( + 𝑋 ) = 𝑘 ) )
46 35 39 45 3bitr4rd ( ( 𝜑𝑘𝐵 ) → ( 𝑘 ∈ ( 𝐴 { 𝑋 } ) ↔ 𝑘 ∈ [ 𝑋 ] ) )
47 11 29 46 eqrdav ( 𝜑 → ( 𝐴 { 𝑋 } ) = [ 𝑋 ] )