Metamath Proof Explorer


Theorem gsumccat

Description: Homomorphic property of composites. Second formula in Lang p. 4. (Contributed by Stefan O'Rear, 16-Aug-2015) (Revised by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 26-Dec-2023)

Ref Expression
Hypotheses gsumccat.b B = Base G
gsumccat.p + ˙ = + G
Assertion gsumccat G Mnd W Word B X Word B G W ++ X = G W + ˙ G X

Proof

Step Hyp Ref Expression
1 gsumccat.b B = Base G
2 gsumccat.p + ˙ = + G
3 oveq1 W = W ++ X = ++ X
4 3 oveq2d W = G W ++ X = G ++ X
5 oveq2 W = G W = G
6 eqid 0 G = 0 G
7 6 gsum0 G = 0 G
8 5 7 eqtrdi W = G W = 0 G
9 8 oveq1d W = G W + ˙ G X = 0 G + ˙ G X
10 4 9 eqeq12d W = G W ++ X = G W + ˙ G X G ++ X = 0 G + ˙ G X
11 oveq2 X = W ++ X = W ++
12 11 oveq2d X = G W ++ X = G W ++
13 oveq2 X = G X = G
14 13 7 eqtrdi X = G X = 0 G
15 14 oveq2d X = G W + ˙ G X = G W + ˙ 0 G
16 12 15 eqeq12d X = G W ++ X = G W + ˙ G X G W ++ = G W + ˙ 0 G
17 mndsgrp Could not format ( G e. Mnd -> G e. Smgrp ) : No typesetting found for |- ( G e. Mnd -> G e. Smgrp ) with typecode |-
18 17 3ad2ant1 Could not format ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> G e. Smgrp ) : No typesetting found for |- ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> G e. Smgrp ) with typecode |-
19 18 ad2antrr Could not format ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) /\ X =/= (/) ) -> G e. Smgrp ) : No typesetting found for |- ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) /\ X =/= (/) ) -> G e. Smgrp ) with typecode |-
20 3simpc G Mnd W Word B X Word B W Word B X Word B
21 20 ad2antrr G Mnd W Word B X Word B W X W Word B X Word B
22 simpr G Mnd W Word B X Word B W W
23 22 anim1i G Mnd W Word B X Word B W X W X
24 1 2 gsumsgrpccat Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) with typecode |-
25 19 21 23 24 syl3anc G Mnd W Word B X Word B W X G W ++ X = G W + ˙ G X
26 simpl2 G Mnd W Word B X Word B W W Word B
27 ccatrid W Word B W ++ = W
28 26 27 syl G Mnd W Word B X Word B W W ++ = W
29 28 oveq2d G Mnd W Word B X Word B W G W ++ = G W
30 simpl1 G Mnd W Word B X Word B W G Mnd
31 1 gsumwcl G Mnd W Word B G W B
32 31 3adant3 G Mnd W Word B X Word B G W B
33 32 adantr G Mnd W Word B X Word B W G W B
34 1 2 6 mndrid G Mnd G W B G W + ˙ 0 G = G W
35 30 33 34 syl2anc G Mnd W Word B X Word B W G W + ˙ 0 G = G W
36 29 35 eqtr4d G Mnd W Word B X Word B W G W ++ = G W + ˙ 0 G
37 16 25 36 pm2.61ne G Mnd W Word B X Word B W G W ++ X = G W + ˙ G X
38 ccatlid X Word B ++ X = X
39 38 3ad2ant3 G Mnd W Word B X Word B ++ X = X
40 39 oveq2d G Mnd W Word B X Word B G ++ X = G X
41 simp1 G Mnd W Word B X Word B G Mnd
42 1 gsumwcl G Mnd X Word B G X B
43 1 2 6 mndlid G Mnd G X B 0 G + ˙ G X = G X
44 41 42 43 3imp3i2an G Mnd W Word B X Word B 0 G + ˙ G X = G X
45 40 44 eqtr4d G Mnd W Word B X Word B G ++ X = 0 G + ˙ G X
46 10 37 45 pm2.61ne G Mnd W Word B X Word B G W ++ X = G W + ˙ G X