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 ) ) ) )