This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⟨“ 𝑆 ”⟩ ) = 𝑆 )