Metamath Proof Explorer

Theorem ghmplusg

Description: The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypothesis ghmplusg.p ⊢ + = ( +g ‘ 𝑁 )
Assertion ghmplusg ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑀 GrpHom 𝑁 ) )

Proof

Step Hyp Ref Expression
1 ghmplusg.p ⊢ + = ( +g ‘ 𝑁 )
2 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3 eqid ⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
4 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
5 ghmgrp1 ⊢ ( 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) → 𝑀 ∈ Grp )
6 5 3ad2ant3 ⊢ ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → 𝑀 ∈ Grp )
7 ghmgrp2 ⊢ ( 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) → 𝑁 ∈ Grp )
8 7 3ad2ant3 ⊢ ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → 𝑁 ∈ Grp )
9 3 1 grpcl ⊢ ( ( 𝑁 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) → ( 𝑥 + 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
10 9 3expb ⊢ ( ( 𝑁 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
11 8 10 sylan ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑁 ) ∧ 𝑦 ∈ ( Base ‘ 𝑁 ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
12 2 3 ghmf ⊢ ( 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
13 12 3ad2ant2 ⊢ ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
14 2 3 ghmf ⊢ ( 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) → 𝐺 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
15 14 3ad2ant3 ⊢ ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → 𝐺 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
16 fvexd ⊢ ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → ( Base ‘ 𝑀 ) ∈ V )
17 inidm ⊢ ( ( Base ‘ 𝑀 ) ∩ ( Base ‘ 𝑀 ) ) = ( Base ‘ 𝑀 )
18 11 13 15 16 16 17 off ⊢ ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → ( 𝐹 ∘f + 𝐺 ) : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
19 2 4 1 ghmlin ⊢ ( ( 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
20 19 3expb ⊢ ( ( 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
21 20 3ad2antl2 ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
22 2 4 1 ghmlin ⊢ ( ( 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑦 ) ) )
23 22 3expb ⊢ ( ( 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑦 ) ) )
24 23 3ad2antl3 ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑦 ) ) )
25 21 24 oveq12d ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) ) = ( ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) + ( ( 𝐺 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑦 ) ) ) )
26 simpl1 ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑁 ∈ Abel )
27 ablcmn ⊢ ( 𝑁 ∈ Abel → 𝑁 ∈ CMnd )
28 26 27 syl ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑁 ∈ CMnd )
29 13 ffvelcdmda ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑁 ) )
30 29 adantrr ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑁 ) )
31 13 ffvelcdmda ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
32 31 adantrl ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
33 15 ffvelcdmda ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑁 ) )
34 33 adantrr ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑁 ) )
35 15 ffvelcdmda ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
36 35 adantrl ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) )
37 3 1 cmn4 ⊢ ( ( 𝑁 ∈ CMnd ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑁 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑁 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) ) → ( ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) + ( ( 𝐺 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑦 ) ) ) = ( ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) + ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) )
38 28 30 32 34 36 37 syl122anc ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) + ( ( 𝐺 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑦 ) ) ) = ( ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) + ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) )
39 25 38 eqtrd ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) ) = ( ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) + ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) )
40 13 ffnd ⊢ ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
41 40 adantr ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
42 15 ffnd ⊢ ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → 𝐺 Fn ( Base ‘ 𝑀 ) )
43 42 adantr ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐺 Fn ( Base ‘ 𝑀 ) )
44 fvexd ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( Base ‘ 𝑀 ) ∈ V )
45 2 4 grpcl ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
46 45 3expb ⊢ ( ( 𝑀 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
47 6 46 sylan ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
48 fnfvof ⊢ ( ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝐺 Fn ( Base ‘ 𝑀 ) ) ∧ ( ( Base ‘ 𝑀 ) ∈ V ∧ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) ) )
49 41 43 44 47 48 syl22anc ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) + ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) ) )
50 simprl ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
51 fnfvof ⊢ ( ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝐺 Fn ( Base ‘ 𝑀 ) ) ∧ ( ( Base ‘ 𝑀 ) ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
52 41 43 44 50 51 syl22anc ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
53 simprr ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑀 ) )
54 fnfvof ⊢ ( ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝐺 Fn ( Base ‘ 𝑀 ) ) ∧ ( ( Base ‘ 𝑀 ) ∈ V ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) )
55 41 43 44 53 54 syl22anc ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) )
56 52 55 oveq12d ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) + ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) + ( ( 𝐹 ‘ 𝑦 ) + ( 𝐺 ‘ 𝑦 ) ) ) )
57 39 49 56 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) = ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) + ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑦 ) ) )
58 2 3 4 1 6 8 18 57 isghmd ⊢ ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑀 GrpHom 𝑁 ) )