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 
|- B = ( Base ` G )
Assertion gsumws1 
|- ( S e. B -> ( G gsum <" S "> ) = S )

Proof

Step Hyp Ref Expression
1 gsumwcl.b 
 |-  B = ( Base ` G )
2 s1val 
 |-  ( S e. B -> <" S "> = { <. 0 , S >. } )
3 2 oveq2d 
 |-  ( S e. B -> ( G gsum <" S "> ) = ( G gsum { <. 0 , S >. } ) )
4 eqid 
 |-  ( +g ` G ) = ( +g ` G )
5 elfvdm 
 |-  ( S e. ( Base ` G ) -> G e. dom Base )
6 5 1 eleq2s 
 |-  ( S e. B -> G e. dom Base )
7 0nn0 
 |-  0 e. NN0
8 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
9 7 8 eleqtri 
 |-  0 e. ( ZZ>= ` 0 )
10 9 a1i 
 |-  ( S e. B -> 0 e. ( ZZ>= ` 0 ) )
11 0z 
 |-  0 e. ZZ
12 f1osng 
 |-  ( ( 0 e. ZZ /\ S e. B ) -> { <. 0 , S >. } : { 0 } -1-1-onto-> { S } )
13 11 12 mpan 
 |-  ( S e. B -> { <. 0 , S >. } : { 0 } -1-1-onto-> { S } )
14 f1of 
 |-  ( { <. 0 , S >. } : { 0 } -1-1-onto-> { S } -> { <. 0 , S >. } : { 0 } --> { S } )
15 13 14 syl 
 |-  ( S e. B -> { <. 0 , S >. } : { 0 } --> { S } )
16 snssi 
 |-  ( S e. B -> { S } C_ B )
17 15 16 fssd 
 |-  ( S e. B -> { <. 0 , S >. } : { 0 } --> B )
18 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
19 18 feq2i 
 |-  ( { <. 0 , S >. } : ( 0 ... 0 ) --> B <-> { <. 0 , S >. } : { 0 } --> B )
20 17 19 sylibr 
 |-  ( S e. B -> { <. 0 , S >. } : ( 0 ... 0 ) --> B )
21 1 4 6 10 20 gsumval2 
 |-  ( S e. B -> ( G gsum { <. 0 , S >. } ) = ( seq 0 ( ( +g ` G ) , { <. 0 , S >. } ) ` 0 ) )
22 fvsng 
 |-  ( ( 0 e. ZZ /\ S e. B ) -> ( { <. 0 , S >. } ` 0 ) = S )
23 11 22 mpan 
 |-  ( S e. B -> ( { <. 0 , S >. } ` 0 ) = S )
24 11 23 seq1i 
 |-  ( S e. B -> ( seq 0 ( ( +g ` G ) , { <. 0 , S >. } ) ` 0 ) = S )
25 3 21 24 3eqtrd 
 |-  ( S e. B -> ( G gsum <" S "> ) = S )