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 𝐵 = ( Base ‘ 𝐺 )
gsumccat.p + = ( +g𝐺 )
Assertion gsumccat ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) → ( 𝐺 Σg ( 𝑊 ++ 𝑋 ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 gsumccat.b 𝐵 = ( Base ‘ 𝐺 )
2 gsumccat.p + = ( +g𝐺 )
3 oveq1 ( 𝑊 = ∅ → ( 𝑊 ++ 𝑋 ) = ( ∅ ++ 𝑋 ) )
4 3 oveq2d ( 𝑊 = ∅ → ( 𝐺 Σg ( 𝑊 ++ 𝑋 ) ) = ( 𝐺 Σg ( ∅ ++ 𝑋 ) ) )
5 oveq2 ( 𝑊 = ∅ → ( 𝐺 Σg 𝑊 ) = ( 𝐺 Σg ∅ ) )
6 eqid ( 0g𝐺 ) = ( 0g𝐺 )
7 6 gsum0 ( 𝐺 Σg ∅ ) = ( 0g𝐺 )
8 5 7 eqtrdi ( 𝑊 = ∅ → ( 𝐺 Σg 𝑊 ) = ( 0g𝐺 ) )
9 8 oveq1d ( 𝑊 = ∅ → ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg 𝑋 ) ) = ( ( 0g𝐺 ) + ( 𝐺 Σg 𝑋 ) ) )
10 4 9 eqeq12d ( 𝑊 = ∅ → ( ( 𝐺 Σg ( 𝑊 ++ 𝑋 ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg 𝑋 ) ) ↔ ( 𝐺 Σg ( ∅ ++ 𝑋 ) ) = ( ( 0g𝐺 ) + ( 𝐺 Σg 𝑋 ) ) ) )
11 oveq2 ( 𝑋 = ∅ → ( 𝑊 ++ 𝑋 ) = ( 𝑊 ++ ∅ ) )
12 11 oveq2d ( 𝑋 = ∅ → ( 𝐺 Σg ( 𝑊 ++ 𝑋 ) ) = ( 𝐺 Σg ( 𝑊 ++ ∅ ) ) )
13 oveq2 ( 𝑋 = ∅ → ( 𝐺 Σg 𝑋 ) = ( 𝐺 Σg ∅ ) )
14 13 7 eqtrdi ( 𝑋 = ∅ → ( 𝐺 Σg 𝑋 ) = ( 0g𝐺 ) )
15 14 oveq2d ( 𝑋 = ∅ → ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg 𝑋 ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 0g𝐺 ) ) )
16 12 15 eqeq12d ( 𝑋 = ∅ → ( ( 𝐺 Σg ( 𝑊 ++ 𝑋 ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg 𝑋 ) ) ↔ ( 𝐺 Σg ( 𝑊 ++ ∅ ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 0g𝐺 ) ) ) )
17 mndsgrp ( 𝐺 ∈ Mnd → 𝐺 ∈ Smgrp )
18 17 3ad2ant1 ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) → 𝐺 ∈ Smgrp )
19 18 ad2antrr ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) ∧ 𝑋 ≠ ∅ ) → 𝐺 ∈ Smgrp )
20 3simpc ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) → ( 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) )
21 20 ad2antrr ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) ∧ 𝑋 ≠ ∅ ) → ( 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) )
22 simpr ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) → 𝑊 ≠ ∅ )
23 22 anim1i ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) ∧ 𝑋 ≠ ∅ ) → ( 𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅ ) )
24 1 2 gsumsgrpccat ( ( 𝐺 ∈ Smgrp ∧ ( 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ ( 𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅ ) ) → ( 𝐺 Σg ( 𝑊 ++ 𝑋 ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg 𝑋 ) ) )
25 19 21 23 24 syl3anc ( ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) ∧ 𝑋 ≠ ∅ ) → ( 𝐺 Σg ( 𝑊 ++ 𝑋 ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg 𝑋 ) ) )
26 simpl2 ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) → 𝑊 ∈ Word 𝐵 )
27 ccatrid ( 𝑊 ∈ Word 𝐵 → ( 𝑊 ++ ∅ ) = 𝑊 )
28 26 27 syl ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) → ( 𝑊 ++ ∅ ) = 𝑊 )
29 28 oveq2d ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) → ( 𝐺 Σg ( 𝑊 ++ ∅ ) ) = ( 𝐺 Σg 𝑊 ) )
30 simpl1 ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) → 𝐺 ∈ Mnd )
31 1 gsumwcl ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ) → ( 𝐺 Σg 𝑊 ) ∈ 𝐵 )
32 31 3adant3 ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) → ( 𝐺 Σg 𝑊 ) ∈ 𝐵 )
33 32 adantr ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) → ( 𝐺 Σg 𝑊 ) ∈ 𝐵 )
34 1 2 6 mndrid ( ( 𝐺 ∈ Mnd ∧ ( 𝐺 Σg 𝑊 ) ∈ 𝐵 ) → ( ( 𝐺 Σg 𝑊 ) + ( 0g𝐺 ) ) = ( 𝐺 Σg 𝑊 ) )
35 30 33 34 syl2anc ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) → ( ( 𝐺 Σg 𝑊 ) + ( 0g𝐺 ) ) = ( 𝐺 Σg 𝑊 ) )
36 29 35 eqtr4d ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) → ( 𝐺 Σg ( 𝑊 ++ ∅ ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 0g𝐺 ) ) )
37 16 25 36 pm2.61ne ( ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) ∧ 𝑊 ≠ ∅ ) → ( 𝐺 Σg ( 𝑊 ++ 𝑋 ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg 𝑋 ) ) )
38 ccatlid ( 𝑋 ∈ Word 𝐵 → ( ∅ ++ 𝑋 ) = 𝑋 )
39 38 3ad2ant3 ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) → ( ∅ ++ 𝑋 ) = 𝑋 )
40 39 oveq2d ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) → ( 𝐺 Σg ( ∅ ++ 𝑋 ) ) = ( 𝐺 Σg 𝑋 ) )
41 simp1 ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) → 𝐺 ∈ Mnd )
42 1 gsumwcl ( ( 𝐺 ∈ Mnd ∧ 𝑋 ∈ Word 𝐵 ) → ( 𝐺 Σg 𝑋 ) ∈ 𝐵 )
43 1 2 6 mndlid ( ( 𝐺 ∈ Mnd ∧ ( 𝐺 Σg 𝑋 ) ∈ 𝐵 ) → ( ( 0g𝐺 ) + ( 𝐺 Σg 𝑋 ) ) = ( 𝐺 Σg 𝑋 ) )
44 41 42 43 3imp3i2an ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) → ( ( 0g𝐺 ) + ( 𝐺 Σg 𝑋 ) ) = ( 𝐺 Σg 𝑋 ) )
45 40 44 eqtr4d ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) → ( 𝐺 Σg ( ∅ ++ 𝑋 ) ) = ( ( 0g𝐺 ) + ( 𝐺 Σg 𝑋 ) ) )
46 10 37 45 pm2.61ne ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵 ) → ( 𝐺 Σg ( 𝑊 ++ 𝑋 ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg 𝑋 ) ) )