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	⊢ ( opp_g ‘ 𝐺 ) = ( opp_g ‘ 𝐺 )
9	8 3	oppglsm	⊢ ( 𝐴 ( LSSum ‘ ( opp_g ‘ 𝐺 ) ) { 𝑋 } ) = ( { 𝑋 } ⊕ 𝐴 )
10	8 1	oppgbas	⊢ 𝐵 = ( Base ‘ ( opp_g ‘ 𝐺 ) )
11		eqid	⊢ ( +_g ‘ ( opp_g ‘ 𝐺 ) ) = ( +_g ‘ ( opp_g ‘ 𝐺 ) )
12		eqid	⊢ ( LSSum ‘ ( opp_g ‘ 𝐺 ) ) = ( LSSum ‘ ( opp_g ‘ 𝐺 ) )
13	2 8 11	oppgplus	⊢ ( 𝑔 ( +_g ‘ ( opp_g ‘ 𝐺 ) ) 𝑥 ) = ( 𝑥 + 𝑔 )
14	13	eqeq1i	⊢ ( ( 𝑔 ( +_g ‘ ( opp_g ‘ 𝐺 ) ) 𝑥 ) = 𝑦 ↔ ( 𝑥 + 𝑔 ) = 𝑦 )
15	14	rexbii	⊢ ( ∃ 𝑔 ∈ 𝐴 ( 𝑔 ( +_g ‘ ( opp_g ‘ 𝐺 ) ) 𝑥 ) = 𝑦 ↔ ∃ 𝑔 ∈ 𝐴 ( 𝑥 + 𝑔 ) = 𝑦 )
16	15	anbi2i	⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 ( +_g ‘ ( opp_g ‘ 𝐺 ) ) 𝑥 ) = 𝑦 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑥 + 𝑔 ) = 𝑦 ) )
17	16	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 ( +_g ‘ ( opp_g ‘ 𝐺 ) ) 𝑥 ) = 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑥 + 𝑔 ) = 𝑦 ) }
18	4 17	eqtr4i	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 ( +_g ‘ ( opp_g ‘ 𝐺 ) ) 𝑥 ) = 𝑦 ) }
19	8	oppgmnd	⊢ ( 𝐺 ∈ Mnd → ( opp_g ‘ 𝐺 ) ∈ Mnd )
20	5 19	syl	⊢ ( 𝜑 → ( opp_g ‘ 𝐺 ) ∈ Mnd )
21	10 11 12 18 20 6 7	lsmsnorb	⊢ ( 𝜑 → ( 𝐴 ( LSSum ‘ ( opp_g ‘ 𝐺 ) ) { 𝑋 } ) = [ 𝑋 ] ∼ )
22	9 21	eqtr3id	⊢ ( 𝜑 → ( { 𝑋 } ⊕ 𝐴 ) = [ 𝑋 ] ∼ )

Metamath Proof Explorer

Theorem lsmsnorb2

Proof