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

Proof

Step Hyp Ref Expression
1 lsmsnorb2.1 𝐵 = ( Base ‘ 𝐺 )
2 lsmsnorb2.2 + = ( +g𝐺 )
3 lsmsnorb2.3 = ( LSSum ‘ 𝐺 )
4 lsmsnorb2.4 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑥 + 𝑔 ) = 𝑦 ) }
5 lsmsnorb2.5 ( 𝜑𝐺 ∈ Mnd )
6 lsmsnorb2.6 ( 𝜑𝐴𝐵 )
7 lsmsnorb2.7 ( 𝜑𝑋𝐵 )
8 eqid ( oppg𝐺 ) = ( oppg𝐺 )
9 8 3 oppglsm ( 𝐴 ( LSSum ‘ ( oppg𝐺 ) ) { 𝑋 } ) = ( { 𝑋 } 𝐴 )
10 8 1 oppgbas 𝐵 = ( Base ‘ ( oppg𝐺 ) )
11 eqid ( +g ‘ ( oppg𝐺 ) ) = ( +g ‘ ( oppg𝐺 ) )
12 eqid ( LSSum ‘ ( oppg𝐺 ) ) = ( LSSum ‘ ( oppg𝐺 ) )
13 2 8 11 oppgplus ( 𝑔 ( +g ‘ ( oppg𝐺 ) ) 𝑥 ) = ( 𝑥 + 𝑔 )
14 13 eqeq1i ( ( 𝑔 ( +g ‘ ( oppg𝐺 ) ) 𝑥 ) = 𝑦 ↔ ( 𝑥 + 𝑔 ) = 𝑦 )
15 14 rexbii ( ∃ 𝑔𝐴 ( 𝑔 ( +g ‘ ( oppg𝐺 ) ) 𝑥 ) = 𝑦 ↔ ∃ 𝑔𝐴 ( 𝑥 + 𝑔 ) = 𝑦 )
16 15 anbi2i ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 ( +g ‘ ( oppg𝐺 ) ) 𝑥 ) = 𝑦 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑥 + 𝑔 ) = 𝑦 ) )
17 16 opabbii { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 ( +g ‘ ( oppg𝐺 ) ) 𝑥 ) = 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑥 + 𝑔 ) = 𝑦 ) }
18 4 17 eqtr4i = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔𝐴 ( 𝑔 ( +g ‘ ( oppg𝐺 ) ) 𝑥 ) = 𝑦 ) }
19 8 oppgmnd ( 𝐺 ∈ Mnd → ( oppg𝐺 ) ∈ Mnd )
20 5 19 syl ( 𝜑 → ( oppg𝐺 ) ∈ Mnd )
21 10 11 12 18 20 6 7 lsmsnorb ( 𝜑 → ( 𝐴 ( LSSum ‘ ( oppg𝐺 ) ) { 𝑋 } ) = [ 𝑋 ] )
22 9 21 eqtr3id ( 𝜑 → ( { 𝑋 } 𝐴 ) = [ 𝑋 ] )