This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmn145236

Description: Rearrange terms in a commutative monoid sum. Lemma for rlocaddval . (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses cmn135246.1 
|- B = ( Base ` G )
cmn135246.2 
|- .+ = ( +g ` G )
cmn135246.3 
|- ( ph -> G e. CMnd )
cmn135246.5 
|- ( ph -> X e. B )
cmn135246.4 
|- ( ph -> Y e. B )
cmn135246.6 
|- ( ph -> Z e. B )
cmn135246.7 
|- ( ph -> U e. B )
cmn135246.8 
|- ( ph -> V e. B )
cmn135246.9 
|- ( ph -> W e. B )
Assertion cmn145236 
|- ( ph -> ( ( X .+ Y ) .+ ( ( Z .+ U ) .+ ( V .+ W ) ) ) = ( ( X .+ ( U .+ V ) ) .+ ( Y .+ ( Z .+ W ) ) ) )

Proof

Step Hyp Ref Expression
1 cmn135246.1 
 |-  B = ( Base ` G )
2 cmn135246.2 
 |-  .+ = ( +g ` G )
3 cmn135246.3 
 |-  ( ph -> G e. CMnd )
4 cmn135246.5 
 |-  ( ph -> X e. B )
5 cmn135246.4 
 |-  ( ph -> Y e. B )
6 cmn135246.6 
 |-  ( ph -> Z e. B )
7 cmn135246.7 
 |-  ( ph -> U e. B )
8 cmn135246.8 
 |-  ( ph -> V e. B )
9 cmn135246.9 
 |-  ( ph -> W e. B )
10 1 2 cmncom 
 |-  ( ( G e. CMnd /\ Z e. B /\ U e. B ) -> ( Z .+ U ) = ( U .+ Z ) )
11 3 6 7 10 syl3anc 
 |-  ( ph -> ( Z .+ U ) = ( U .+ Z ) )
12 11 oveq1d 
 |-  ( ph -> ( ( Z .+ U ) .+ ( V .+ W ) ) = ( ( U .+ Z ) .+ ( V .+ W ) ) )
13 1 2 3 7 6 8 9 cmn4d 
 |-  ( ph -> ( ( U .+ Z ) .+ ( V .+ W ) ) = ( ( U .+ V ) .+ ( Z .+ W ) ) )
14 12 13 eqtrd 
 |-  ( ph -> ( ( Z .+ U ) .+ ( V .+ W ) ) = ( ( U .+ V ) .+ ( Z .+ W ) ) )
15 14 oveq2d 
 |-  ( ph -> ( ( X .+ Y ) .+ ( ( Z .+ U ) .+ ( V .+ W ) ) ) = ( ( X .+ Y ) .+ ( ( U .+ V ) .+ ( Z .+ W ) ) ) )
16 3 cmnmndd 
 |-  ( ph -> G e. Mnd )
17 1 2 mndcl 
 |-  ( ( G e. Mnd /\ U e. B /\ V e. B ) -> ( U .+ V ) e. B )
18 16 7 8 17 syl3anc 
 |-  ( ph -> ( U .+ V ) e. B )
19 1 2 mndcl 
 |-  ( ( G e. Mnd /\ Z e. B /\ W e. B ) -> ( Z .+ W ) e. B )
20 16 6 9 19 syl3anc 
 |-  ( ph -> ( Z .+ W ) e. B )
21 1 2 3 4 18 5 20 cmn4d 
 |-  ( ph -> ( ( X .+ ( U .+ V ) ) .+ ( Y .+ ( Z .+ W ) ) ) = ( ( X .+ Y ) .+ ( ( U .+ V ) .+ ( Z .+ W ) ) ) )
22 15 21 eqtr4d 
 |-  ( ph -> ( ( X .+ Y ) .+ ( ( Z .+ U ) .+ ( V .+ W ) ) ) = ( ( X .+ ( U .+ V ) ) .+ ( Y .+ ( Z .+ W ) ) ) )