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	⊢ ( 𝜑 → ( 𝐴 ⊕ { 𝑋 } ) = [ 𝑋 ] ∼ )

Metamath Proof Explorer

Theorem lsmsnorb

Proof