Metamath Proof Explorer

Theorem gsumzresunsn

Description: Append an element to a finite group sum expressed as a function restriction. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Hypotheses gsumzresunsn.b 
|- B = ( Base ` G )
gsumzresunsn.p 
|- .+ = ( +g ` G )
gsumzresunsn.z 
|- Z = ( Cntz ` G )
gsumzresunsn.y 
|- Y = ( F ` X )
gsumzresunsn.f 
|- ( ph -> F : C --> B )
gsumzresunsn.1 
|- ( ph -> A C_ C )
gsumzresunsn.g 
|- ( ph -> G e. Mnd )
gsumzresunsn.a 
|- ( ph -> A e. Fin )
gsumzresunsn.2 
|- ( ph -> -. X e. A )
gsumzresunsn.3 
|- ( ph -> X e. C )
gsumzresunsn.4 
|- ( ph -> Y e. B )
gsumzresunsn.5 
|- ( ph -> ( F " ( A u. { X } ) ) C_ ( Z ` ( F " ( A u. { X } ) ) ) )
Assertion gsumzresunsn 
|- ( ph -> ( G gsum ( F |` ( A u. { X } ) ) ) = ( ( G gsum ( F |` A ) ) .+ Y ) )

Proof

Step Hyp Ref Expression
1 gsumzresunsn.b 
 |-  B = ( Base ` G )
2 gsumzresunsn.p 
 |-  .+ = ( +g ` G )
3 gsumzresunsn.z 
 |-  Z = ( Cntz ` G )
4 gsumzresunsn.y 
 |-  Y = ( F ` X )
5 gsumzresunsn.f 
 |-  ( ph -> F : C --> B )
6 gsumzresunsn.1 
 |-  ( ph -> A C_ C )
7 gsumzresunsn.g 
 |-  ( ph -> G e. Mnd )
8 gsumzresunsn.a 
 |-  ( ph -> A e. Fin )
9 gsumzresunsn.2 
 |-  ( ph -> -. X e. A )
10 gsumzresunsn.3 
 |-  ( ph -> X e. C )
11 gsumzresunsn.4 
 |-  ( ph -> Y e. B )
12 gsumzresunsn.5 
 |-  ( ph -> ( F " ( A u. { X } ) ) C_ ( Z ` ( F " ( A u. { X } ) ) ) )
13 eqid 
 |-  ( x e. ( A u. { X } ) |-> ( F ` x ) ) = ( x e. ( A u. { X } ) |-> ( F ` x ) )
14 df-ima 
 |-  ( F " ( A u. { X } ) ) = ran ( F |` ( A u. { X } ) )
15 10 snssd 
 |-  ( ph -> { X } C_ C )
16 6 15 unssd 
 |-  ( ph -> ( A u. { X } ) C_ C )
17 5 16 feqresmpt 
 |-  ( ph -> ( F |` ( A u. { X } ) ) = ( x e. ( A u. { X } ) |-> ( F ` x ) ) )
18 17 rneqd 
 |-  ( ph -> ran ( F |` ( A u. { X } ) ) = ran ( x e. ( A u. { X } ) |-> ( F ` x ) ) )
19 14 18 syl5eq 
 |-  ( ph -> ( F " ( A u. { X } ) ) = ran ( x e. ( A u. { X } ) |-> ( F ` x ) ) )
20 19 fveq2d 
 |-  ( ph -> ( Z ` ( F " ( A u. { X } ) ) ) = ( Z ` ran ( x e. ( A u. { X } ) |-> ( F ` x ) ) ) )
21 12 19 20 3sstr3d 
 |-  ( ph -> ran ( x e. ( A u. { X } ) |-> ( F ` x ) ) C_ ( Z ` ran ( x e. ( A u. { X } ) |-> ( F ` x ) ) ) )
22 5 adantr 
 |-  ( ( ph /\ x e. A ) -> F : C --> B )
23 6 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. C )
24 22 23 ffvelrnd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
25 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
26 25 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( F ` x ) = ( F ` X ) )
27 26 4 eqtr4di 
 |-  ( ( ph /\ x = X ) -> ( F ` x ) = Y )
28 1 2 3 13 7 8 21 24 10 9 11 27 gsumzunsnd 
 |-  ( ph -> ( G gsum ( x e. ( A u. { X } ) |-> ( F ` x ) ) ) = ( ( G gsum ( x e. A |-> ( F ` x ) ) ) .+ Y ) )
29 17 oveq2d 
 |-  ( ph -> ( G gsum ( F |` ( A u. { X } ) ) ) = ( G gsum ( x e. ( A u. { X } ) |-> ( F ` x ) ) ) )
30 5 6 feqresmpt 
 |-  ( ph -> ( F |` A ) = ( x e. A |-> ( F ` x ) ) )
31 30 oveq2d 
 |-  ( ph -> ( G gsum ( F |` A ) ) = ( G gsum ( x e. A |-> ( F ` x ) ) ) )
32 31 oveq1d 
 |-  ( ph -> ( ( G gsum ( F |` A ) ) .+ Y ) = ( ( G gsum ( x e. A |-> ( F ` x ) ) ) .+ Y ) )
33 28 29 32 3eqtr4d 
 |-  ( ph -> ( G gsum ( F |` ( A u. { X } ) ) ) = ( ( G gsum ( F |` A ) ) .+ Y ) )