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

Metamath Proof Explorer

Theorem cmn246135

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 cmn246135 
|- ( ph -> ( ( X .+ Y ) .+ ( ( Z .+ U ) .+ ( V .+ W ) ) ) = ( ( Y .+ ( U .+ W ) ) .+ ( X .+ ( Z .+ V ) ) ) )

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 /\ X e. B /\ Y e. B ) -> ( X .+ Y ) = ( Y .+ X ) )
11 3 4 5 10 syl3anc 
 |-  ( ph -> ( X .+ Y ) = ( Y .+ X ) )
12 1 2 3 6 7 8 9 cmn4d 
 |-  ( ph -> ( ( Z .+ U ) .+ ( V .+ W ) ) = ( ( Z .+ V ) .+ ( U .+ W ) ) )
13 3 cmnmndd 
 |-  ( ph -> G e. Mnd )
14 1 2 mndcl 
 |-  ( ( G e. Mnd /\ Z e. B /\ V e. B ) -> ( Z .+ V ) e. B )
15 13 6 8 14 syl3anc 
 |-  ( ph -> ( Z .+ V ) e. B )
16 1 2 mndcl 
 |-  ( ( G e. Mnd /\ U e. B /\ W e. B ) -> ( U .+ W ) e. B )
17 13 7 9 16 syl3anc 
 |-  ( ph -> ( U .+ W ) e. B )
18 1 2 cmncom 
 |-  ( ( G e. CMnd /\ ( Z .+ V ) e. B /\ ( U .+ W ) e. B ) -> ( ( Z .+ V ) .+ ( U .+ W ) ) = ( ( U .+ W ) .+ ( Z .+ V ) ) )
19 3 15 17 18 syl3anc 
 |-  ( ph -> ( ( Z .+ V ) .+ ( U .+ W ) ) = ( ( U .+ W ) .+ ( Z .+ V ) ) )
20 12 19 eqtrd 
 |-  ( ph -> ( ( Z .+ U ) .+ ( V .+ W ) ) = ( ( U .+ W ) .+ ( Z .+ V ) ) )
21 11 20 oveq12d 
 |-  ( ph -> ( ( X .+ Y ) .+ ( ( Z .+ U ) .+ ( V .+ W ) ) ) = ( ( Y .+ X ) .+ ( ( U .+ W ) .+ ( Z .+ V ) ) ) )
22 1 2 3 5 4 17 15 cmn4d 
 |-  ( ph -> ( ( Y .+ X ) .+ ( ( U .+ W ) .+ ( Z .+ V ) ) ) = ( ( Y .+ ( U .+ W ) ) .+ ( X .+ ( Z .+ V ) ) ) )
23 21 22 eqtrd 
 |-  ( ph -> ( ( X .+ Y ) .+ ( ( Z .+ U ) .+ ( V .+ W ) ) ) = ( ( Y .+ ( U .+ W ) ) .+ ( X .+ ( Z .+ V ) ) ) )