Metamath Proof Explorer

Theorem gsumunsnfd

Description: Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 11-Dec-2019)

Ref Expression
Hypotheses gsumunsnd.b 
|- B = ( Base ` G )
gsumunsnd.p 
|- .+ = ( +g ` G )
gsumunsnd.g 
|- ( ph -> G e. CMnd )
gsumunsnd.a 
|- ( ph -> A e. Fin )
gsumunsnd.f 
|- ( ( ph /\ k e. A ) -> X e. B )
gsumunsnd.m 
|- ( ph -> M e. V )
gsumunsnd.d 
|- ( ph -> -. M e. A )
gsumunsnd.y 
|- ( ph -> Y e. B )
gsumunsnd.s 
|- ( ( ph /\ k = M ) -> X = Y )
gsumunsnfd.0 
|- F/_ k Y
Assertion gsumunsnfd 
|- ( ph -> ( G gsum ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ Y ) )

Proof

Step Hyp Ref Expression
1 gsumunsnd.b 
 |-  B = ( Base ` G )
2 gsumunsnd.p 
 |-  .+ = ( +g ` G )
3 gsumunsnd.g 
 |-  ( ph -> G e. CMnd )
4 gsumunsnd.a 
 |-  ( ph -> A e. Fin )
5 gsumunsnd.f 
 |-  ( ( ph /\ k e. A ) -> X e. B )
6 gsumunsnd.m 
 |-  ( ph -> M e. V )
7 gsumunsnd.d 
 |-  ( ph -> -. M e. A )
8 gsumunsnd.y 
 |-  ( ph -> Y e. B )
9 gsumunsnd.s 
 |-  ( ( ph /\ k = M ) -> X = Y )
10 gsumunsnfd.0 
 |-  F/_ k Y
11 snfi 
 |-  { M } e. Fin
12 unfi 
 |-  ( ( A e. Fin /\ { M } e. Fin ) -> ( A u. { M } ) e. Fin )
13 4 11 12 sylancl 
 |-  ( ph -> ( A u. { M } ) e. Fin )
14 elun 
 |-  ( k e. ( A u. { M } ) <-> ( k e. A \/ k e. { M } ) )
15 elsni 
 |-  ( k e. { M } -> k = M )
16 15 9 sylan2 
 |-  ( ( ph /\ k e. { M } ) -> X = Y )
17 8 adantr 
 |-  ( ( ph /\ k e. { M } ) -> Y e. B )
18 16 17 eqeltrd 
 |-  ( ( ph /\ k e. { M } ) -> X e. B )
19 5 18 jaodan 
 |-  ( ( ph /\ ( k e. A \/ k e. { M } ) ) -> X e. B )
20 14 19 sylan2b 
 |-  ( ( ph /\ k e. ( A u. { M } ) ) -> X e. B )
21 disjsn 
 |-  ( ( A i^i { M } ) = (/) <-> -. M e. A )
22 7 21 sylibr 
 |-  ( ph -> ( A i^i { M } ) = (/) )
23 eqidd 
 |-  ( ph -> ( A u. { M } ) = ( A u. { M } ) )
24 1 2 3 13 20 22 23 gsummptfidmsplit 
 |-  ( ph -> ( G gsum ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ ( G gsum ( k e. { M } |-> X ) ) ) )
25 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
26 3 25 syl 
 |-  ( ph -> G e. Mnd )
27 nfv 
 |-  F/ k ph
28 1 26 6 8 9 27 10 gsumsnfd 
 |-  ( ph -> ( G gsum ( k e. { M } |-> X ) ) = Y )
29 28 oveq2d 
 |-  ( ph -> ( ( G gsum ( k e. A |-> X ) ) .+ ( G gsum ( k e. { M } |-> X ) ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ Y ) )
30 24 29 eqtrd 
 |-  ( ph -> ( G gsum ( k e. ( A u. { M } ) |-> X ) ) = ( ( G gsum ( k e. A |-> X ) ) .+ Y ) )