Metamath Proof Explorer

Theorem gsumtp

Description: Group sum of an unordered triple. (Contributed by Thierry Arnoux, 22-Jun-2025)

Ref Expression
Hypotheses gsumtp.b 
|- B = ( Base ` G )
gsumtp.p 
|- .+ = ( +g ` G )
gsumtp.s 
|- ( k = M -> A = C )
gsumtp.t 
|- ( k = N -> A = D )
gsumtp.u 
|- ( k = O -> A = E )
gsumtp.1 
|- ( ph -> G e. CMnd )
gsumtp.2 
|- ( ph -> M e. V )
gsumtp.3 
|- ( ph -> N e. W )
gsumtp.4 
|- ( ph -> O e. X )
gsumtp.5 
|- ( ph -> M =/= N )
gsumtp.6 
|- ( ph -> N =/= O )
gsumtp.7 
|- ( ph -> M =/= O )
gsumtp.8 
|- ( ph -> C e. B )
gsumtp.9 
|- ( ph -> D e. B )
gsumtp.10 
|- ( ph -> E e. B )
Assertion gsumtp 
|- ( ph -> ( G gsum ( k e. { M , N , O } |-> A ) ) = ( ( C .+ D ) .+ E ) )

Proof

Step Hyp Ref Expression
1 gsumtp.b 
 |-  B = ( Base ` G )
2 gsumtp.p 
 |-  .+ = ( +g ` G )
3 gsumtp.s 
 |-  ( k = M -> A = C )
4 gsumtp.t 
 |-  ( k = N -> A = D )
5 gsumtp.u 
 |-  ( k = O -> A = E )
6 gsumtp.1 
 |-  ( ph -> G e. CMnd )
7 gsumtp.2 
 |-  ( ph -> M e. V )
8 gsumtp.3 
 |-  ( ph -> N e. W )
9 gsumtp.4 
 |-  ( ph -> O e. X )
10 gsumtp.5 
 |-  ( ph -> M =/= N )
11 gsumtp.6 
 |-  ( ph -> N =/= O )
12 gsumtp.7 
 |-  ( ph -> M =/= O )
13 gsumtp.8 
 |-  ( ph -> C e. B )
14 gsumtp.9 
 |-  ( ph -> D e. B )
15 gsumtp.10 
 |-  ( ph -> E e. B )
16 tpfi 
 |-  { M , N , O } e. Fin
17 16 a1i 
 |-  ( ph -> { M , N , O } e. Fin )
18 3 adantl 
 |-  ( ( ( ph /\ k e. { M , N , O } ) /\ k = M ) -> A = C )
19 13 ad2antrr 
 |-  ( ( ( ph /\ k e. { M , N , O } ) /\ k = M ) -> C e. B )
20 18 19 eqeltrd 
 |-  ( ( ( ph /\ k e. { M , N , O } ) /\ k = M ) -> A e. B )
21 4 adantl 
 |-  ( ( ( ph /\ k e. { M , N , O } ) /\ k = N ) -> A = D )
22 14 ad2antrr 
 |-  ( ( ( ph /\ k e. { M , N , O } ) /\ k = N ) -> D e. B )
23 21 22 eqeltrd 
 |-  ( ( ( ph /\ k e. { M , N , O } ) /\ k = N ) -> A e. B )
24 5 adantl 
 |-  ( ( ( ph /\ k e. { M , N , O } ) /\ k = O ) -> A = E )
25 15 ad2antrr 
 |-  ( ( ( ph /\ k e. { M , N , O } ) /\ k = O ) -> E e. B )
26 24 25 eqeltrd 
 |-  ( ( ( ph /\ k e. { M , N , O } ) /\ k = O ) -> A e. B )
27 eltpi 
 |-  ( k e. { M , N , O } -> ( k = M \/ k = N \/ k = O ) )
28 27 adantl 
 |-  ( ( ph /\ k e. { M , N , O } ) -> ( k = M \/ k = N \/ k = O ) )
29 20 23 26 28 mpjao3dan 
 |-  ( ( ph /\ k e. { M , N , O } ) -> A e. B )
30 disjprsn 
 |-  ( ( M =/= O /\ N =/= O ) -> ( { M , N } i^i { O } ) = (/) )
31 12 11 30 syl2anc 
 |-  ( ph -> ( { M , N } i^i { O } ) = (/) )
32 df-tp 
 |-  { M , N , O } = ( { M , N } u. { O } )
33 32 a1i 
 |-  ( ph -> { M , N , O } = ( { M , N } u. { O } ) )
34 1 2 6 17 29 31 33 gsummptfidmsplit 
 |-  ( ph -> ( G gsum ( k e. { M , N , O } |-> A ) ) = ( ( G gsum ( k e. { M , N } |-> A ) ) .+ ( G gsum ( k e. { O } |-> A ) ) ) )
35 1 2 3 4 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 ) )
36 6 7 8 10 13 14 35 syl132anc 
 |-  ( ph -> ( G gsum ( k e. { M , N } |-> A ) ) = ( C .+ D ) )
37 6 cmnmndd 
 |-  ( ph -> G e. Mnd )
38 5 adantl 
 |-  ( ( ph /\ k = O ) -> A = E )
39 1 37 9 15 38 gsumsnd 
 |-  ( ph -> ( G gsum ( k e. { O } |-> A ) ) = E )
40 36 39 oveq12d 
 |-  ( ph -> ( ( G gsum ( k e. { M , N } |-> A ) ) .+ ( G gsum ( k e. { O } |-> A ) ) ) = ( ( C .+ D ) .+ E ) )
41 34 40 eqtrd 
 |-  ( ph -> ( G gsum ( k e. { M , N , O } |-> A ) ) = ( ( C .+ D ) .+ E ) )