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 ` G )
Assertion gsumccat 
|- ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) )

Proof

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