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
|
ffvelrnda |
⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑁 ) ) |
30 |
29
|
adantrr |
⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑁 ) ) |
31 |
13
|
ffvelrnda |
⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) |
32 |
31
|
adantrl |
⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) |
33 |
15
|
ffvelrnda |
⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑁 ) ) |
34 |
33
|
adantrr |
⊢ ( ( ( 𝑁 ∈ Abel ∧ 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑁 ) ) |
35 |
15
|
ffvelrnda |
⊢ ( ( ( 𝑁 ∈ 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 𝑁 ) ) |