Theorem gsumws1

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

	Ref	Expression
Hypothesis	gsumwcl.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	gsumws1	$$⊢S\in B\to {\sum }_G⟨“S”⟩=S$$

Proof

Step	Hyp	Ref	Expression
1		gsumwcl.b	$$⊢B={\mathrm{Base}}_G$$
2		s1val	$$⊢S\in B\to ⟨“S”⟩=\left\{⟨0,S⟩\right\}$$
3	2	oveq2d	$$⊢S\in B\to {\sum }_G⟨“S”⟩={\sum }_G\left\{⟨0,S⟩\right\}$$
4		eqid	$$⊢{+}_G={+}_G$$
5		elfvdm	$$⊢S\in {\mathrm{Base}}_G\to G\in \mathrm{dom}\mathrm{Base}$$
6	5 1	eleq2s	$$⊢S\in B\to G\in \mathrm{dom}\mathrm{Base}$$
7		0nn0	$$⊢0\in {\mathbb{N}}_0$$
8		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
9	7 8	eleqtri	$$⊢0\in {\mathbb{Z}}_{\ge 0}$$
10	9	a1i	$$⊢S\in B\to 0\in {\mathbb{Z}}_{\ge 0}$$
11		0z	$$⊢0\in \mathbb{Z}$$
12		f1osng	$$⊢\left(0\in \mathbb{Z}\wedge S\in B\right)\to \left\{⟨0,S⟩\right\}:\left\{0\right\}\underset{1-1\; onto}{⟶}\left\{S\right\}$$
13	11 12	mpan	$$⊢S\in B\to \left\{⟨0,S⟩\right\}:\left\{0\right\}\underset{1-1\; onto}{⟶}\left\{S\right\}$$
14		f1of	$$⊢\left\{⟨0,S⟩\right\}:\left\{0\right\}\underset{1-1\; onto}{⟶}\left\{S\right\}\to \left\{⟨0,S⟩\right\}:\left\{0\right\}⟶\left\{S\right\}$$
15	13 14	syl	$$⊢S\in B\to \left\{⟨0,S⟩\right\}:\left\{0\right\}⟶\left\{S\right\}$$
16		snssi	$$⊢S\in B\to \left\{S\right\}\subseteq B$$
17	15 16	fssd	$$⊢S\in B\to \left\{⟨0,S⟩\right\}:\left\{0\right\}⟶B$$
18		fz0sn	$$⊢\left(0\dots 0\right)=\left\{0\right\}$$
19	18	feq2i	$$⊢\left\{⟨0,S⟩\right\}:\left(0\dots 0\right)⟶B\leftrightarrow \left\{⟨0,S⟩\right\}:\left\{0\right\}⟶B$$
20	17 19	sylibr	$$⊢S\in B\to \left\{⟨0,S⟩\right\}:\left(0\dots 0\right)⟶B$$
21	1 4 6 10 20	gsumval2	$$⊢S\in B\to {\sum }_G\left\{⟨0,S⟩\right\}=seq0\left({+}_G,\left\{⟨0,S⟩\right\}\right)\left(0\right)$$
22		fvsng	$$⊢\left(0\in \mathbb{Z}\wedge S\in B\right)\to \left\{⟨0,S⟩\right\}\left(0\right)=S$$
23	11 22	mpan	$$⊢S\in B\to \left\{⟨0,S⟩\right\}\left(0\right)=S$$
24	11 23	seq1i	$$⊢S\in B\to seq0\left({+}_G,\left\{⟨0,S⟩\right\}\right)\left(0\right)=S$$
25	3 21 24	3eqtrd	$$⊢S\in B\to {\sum }_G⟨“S”⟩=S$$