gsumws1

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

		Ref	Expression
	Hypothesis	gsumwcl.b	$⊢ B = {Base}_{G}$
	Assertion	gsumws1	$⊢ S \in B \to \sum_{G} ⟨“ S ”⟩ = S$

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

Metamath Proof Explorer