Theorem gsumws1

Description: A singleton composite recovers the initial symbol. (Contributed by Stefan O'Rear, 16-Aug-2015)

	Ref	Expression
Hypothesis	gsumwcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	gsumws1	⊢ ( 𝑆 ∈ 𝐵 → ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		gsumwcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		s1val	⊢ ( 𝑆 ∈ 𝐵 → ⟨“ 𝑆 ”⟩ = { ⟨ 0 , 𝑆 ⟩ } )
3	2	oveq2d	⊢ ( 𝑆 ∈ 𝐵 → ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) = ( 𝐺 Σg { ⟨ 0 , 𝑆 ⟩ } ) )
4		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5		elfvdm	⊢ ( 𝑆 ∈ ( Base ‘ 𝐺 ) → 𝐺 ∈ dom Base )
6	5 1	eleq2s	⊢ ( 𝑆 ∈ 𝐵 → 𝐺 ∈ dom Base )
7		0nn0	⊢ 0 ∈ ℕ0
8		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
9	7 8	eleqtri	⊢ 0 ∈ ( ℤ≥ ‘ 0 )
10	9	a1i	⊢ ( 𝑆 ∈ 𝐵 → 0 ∈ ( ℤ≥ ‘ 0 ) )
11		0z	⊢ 0 ∈ ℤ
12		f1osng	⊢ ( ( 0 ∈ ℤ ∧ 𝑆 ∈ 𝐵 ) → { ⟨ 0 , 𝑆 ⟩ } : { 0 } –1-1-onto→ { 𝑆 } )
13	11 12	mpan	⊢ ( 𝑆 ∈ 𝐵 → { ⟨ 0 , 𝑆 ⟩ } : { 0 } –1-1-onto→ { 𝑆 } )
14		f1of	⊢ ( { ⟨ 0 , 𝑆 ⟩ } : { 0 } –1-1-onto→ { 𝑆 } → { ⟨ 0 , 𝑆 ⟩ } : { 0 } ⟶ { 𝑆 } )
15	13 14	syl	⊢ ( 𝑆 ∈ 𝐵 → { ⟨ 0 , 𝑆 ⟩ } : { 0 } ⟶ { 𝑆 } )
16		snssi	⊢ ( 𝑆 ∈ 𝐵 → { 𝑆 } ⊆ 𝐵 )
17	15 16	fssd	⊢ ( 𝑆 ∈ 𝐵 → { ⟨ 0 , 𝑆 ⟩ } : { 0 } ⟶ 𝐵 )
18		fz0sn	⊢ ( 0 ... 0 ) = { 0 }
19	18	feq2i	⊢ ( { ⟨ 0 , 𝑆 ⟩ } : ( 0 ... 0 ) ⟶ 𝐵 ↔ { ⟨ 0 , 𝑆 ⟩ } : { 0 } ⟶ 𝐵 )
20	17 19	sylibr	⊢ ( 𝑆 ∈ 𝐵 → { ⟨ 0 , 𝑆 ⟩ } : ( 0 ... 0 ) ⟶ 𝐵 )
21	1 4 6 10 20	gsumval2	⊢ ( 𝑆 ∈ 𝐵 → ( 𝐺 Σg { ⟨ 0 , 𝑆 ⟩ } ) = ( seq 0 ( ( +g ‘ 𝐺 ) , { ⟨ 0 , 𝑆 ⟩ } ) ‘ 0 ) )
22		fvsng	⊢ ( ( 0 ∈ ℤ ∧ 𝑆 ∈ 𝐵 ) → ( { ⟨ 0 , 𝑆 ⟩ } ‘ 0 ) = 𝑆 )
23	11 22	mpan	⊢ ( 𝑆 ∈ 𝐵 → ( { ⟨ 0 , 𝑆 ⟩ } ‘ 0 ) = 𝑆 )
24	11 23	seq1i	⊢ ( 𝑆 ∈ 𝐵 → ( seq 0 ( ( +g ‘ 𝐺 ) , { ⟨ 0 , 𝑆 ⟩ } ) ‘ 0 ) = 𝑆 )
25	3 21 24	3eqtrd	⊢ ( 𝑆 ∈ 𝐵 → ( 𝐺 Σg ⟨“ 𝑆 ”⟩ ) = 𝑆 )