Metamath Proof Explorer

Theorem gsumpr

Description: Group sum of a pair. (Contributed by AV, 6-Dec-2018) (Proof shortened by AV, 28-Jul-2019)

Ref Expression
Hypotheses gsumpr.b 
|- B = ( Base ` G )
gsumpr.p 
|- .+ = ( +g ` G )
gsumpr.s 
|- ( k = M -> A = C )
gsumpr.t 
|- ( k = N -> A = D )
Assertion gsumpr 
|- ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( G gsum ( k e. { M , N } |-> A ) ) = ( C .+ D ) )

Proof

Step Hyp Ref Expression
1 gsumpr.b 
 |-  B = ( Base ` G )
2 gsumpr.p 
 |-  .+ = ( +g ` G )
3 gsumpr.s 
 |-  ( k = M -> A = C )
4 gsumpr.t 
 |-  ( k = N -> A = D )
5 simp1 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> G e. CMnd )
6 prfi 
 |-  { M , N } e. Fin
7 6 a1i 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> { M , N } e. Fin )
8 vex 
 |-  k e. _V
9 8 elpr 
 |-  ( k e. { M , N } <-> ( k = M \/ k = N ) )
10 eleq1a 
 |-  ( C e. B -> ( A = C -> A e. B ) )
11 10 adantr 
 |-  ( ( C e. B /\ D e. B ) -> ( A = C -> A e. B ) )
12 11 3ad2ant3 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( A = C -> A e. B ) )
13 3 12 syl5com 
 |-  ( k = M -> ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> A e. B ) )
14 eleq1a 
 |-  ( D e. B -> ( A = D -> A e. B ) )
15 14 adantl 
 |-  ( ( C e. B /\ D e. B ) -> ( A = D -> A e. B ) )
16 15 3ad2ant3 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( A = D -> A e. B ) )
17 4 16 syl5com 
 |-  ( k = N -> ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> A e. B ) )
18 13 17 jaoi 
 |-  ( ( k = M \/ k = N ) -> ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> A e. B ) )
19 9 18 sylbi 
 |-  ( k e. { M , N } -> ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> A e. B ) )
20 19 impcom 
 |-  ( ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) /\ k e. { M , N } ) -> A e. B )
21 disjsn2 
 |-  ( M =/= N -> ( { M } i^i { N } ) = (/) )
22 21 3ad2ant3 
 |-  ( ( M e. V /\ N e. W /\ M =/= N ) -> ( { M } i^i { N } ) = (/) )
23 22 3ad2ant2 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( { M } i^i { N } ) = (/) )
24 df-pr 
 |-  { M , N } = ( { M } u. { N } )
25 24 a1i 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> { M , N } = ( { M } u. { N } ) )
26 eqid 
 |-  ( k e. { M , N } |-> A ) = ( k e. { M , N } |-> A )
27 1 2 5 7 20 23 25 26 gsummptfidmsplitres 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( G gsum ( k e. { M , N } |-> A ) ) = ( ( G gsum ( ( k e. { M , N } |-> A ) |` { M } ) ) .+ ( G gsum ( ( k e. { M , N } |-> A ) |` { N } ) ) ) )
28 snsspr1 
 |-  { M } C_ { M , N }
29 resmpt 
 |-  ( { M } C_ { M , N } -> ( ( k e. { M , N } |-> A ) |` { M } ) = ( k e. { M } |-> A ) )
30 28 29 mp1i 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( ( k e. { M , N } |-> A ) |` { M } ) = ( k e. { M } |-> A ) )
31 30 oveq2d 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( G gsum ( ( k e. { M , N } |-> A ) |` { M } ) ) = ( G gsum ( k e. { M } |-> A ) ) )
32 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
33 simp1 
 |-  ( ( M e. V /\ N e. W /\ M =/= N ) -> M e. V )
34 simpl 
 |-  ( ( C e. B /\ D e. B ) -> C e. B )
35 1 3 gsumsn 
 |-  ( ( G e. Mnd /\ M e. V /\ C e. B ) -> ( G gsum ( k e. { M } |-> A ) ) = C )
36 32 33 34 35 syl3an 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( G gsum ( k e. { M } |-> A ) ) = C )
37 31 36 eqtrd 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( G gsum ( ( k e. { M , N } |-> A ) |` { M } ) ) = C )
38 snsspr2 
 |-  { N } C_ { M , N }
39 resmpt 
 |-  ( { N } C_ { M , N } -> ( ( k e. { M , N } |-> A ) |` { N } ) = ( k e. { N } |-> A ) )
40 38 39 mp1i 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( ( k e. { M , N } |-> A ) |` { N } ) = ( k e. { N } |-> A ) )
41 40 oveq2d 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( G gsum ( ( k e. { M , N } |-> A ) |` { N } ) ) = ( G gsum ( k e. { N } |-> A ) ) )
42 simp2 
 |-  ( ( M e. V /\ N e. W /\ M =/= N ) -> N e. W )
43 simpr 
 |-  ( ( C e. B /\ D e. B ) -> D e. B )
44 1 4 gsumsn 
 |-  ( ( G e. Mnd /\ N e. W /\ D e. B ) -> ( G gsum ( k e. { N } |-> A ) ) = D )
45 32 42 43 44 syl3an 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( G gsum ( k e. { N } |-> A ) ) = D )
46 41 45 eqtrd 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( G gsum ( ( k e. { M , N } |-> A ) |` { N } ) ) = D )
47 37 46 oveq12d 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( ( G gsum ( ( k e. { M , N } |-> A ) |` { M } ) ) .+ ( G gsum ( ( k e. { M , N } |-> A ) |` { N } ) ) ) = ( C .+ D ) )
48 27 47 eqtrd 
 |-  ( ( G e. CMnd /\ ( M e. V /\ N e. W /\ M =/= N ) /\ ( C e. B /\ D e. B ) ) -> ( G gsum ( k e. { M , N } |-> A ) ) = ( C .+ D ) )