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