Step |
Hyp |
Ref |
Expression |
1 |
|
nmhmplusg.p |
|- .+ = ( +g ` T ) |
2 |
|
nmhmrcl1 |
|- ( F e. ( S NMHom T ) -> S e. NrmMod ) |
3 |
|
nmhmrcl2 |
|- ( G e. ( S NMHom T ) -> T e. NrmMod ) |
4 |
2 3
|
anim12i |
|- ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( S e. NrmMod /\ T e. NrmMod ) ) |
5 |
|
nmhmlmhm |
|- ( F e. ( S NMHom T ) -> F e. ( S LMHom T ) ) |
6 |
|
nmhmlmhm |
|- ( G e. ( S NMHom T ) -> G e. ( S LMHom T ) ) |
7 |
1
|
lmhmplusg |
|- ( ( F e. ( S LMHom T ) /\ G e. ( S LMHom T ) ) -> ( F oF .+ G ) e. ( S LMHom T ) ) |
8 |
5 6 7
|
syl2an |
|- ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( F oF .+ G ) e. ( S LMHom T ) ) |
9 |
|
nlmlmod |
|- ( T e. NrmMod -> T e. LMod ) |
10 |
|
lmodabl |
|- ( T e. LMod -> T e. Abel ) |
11 |
3 9 10
|
3syl |
|- ( G e. ( S NMHom T ) -> T e. Abel ) |
12 |
11
|
adantl |
|- ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> T e. Abel ) |
13 |
|
nmhmnghm |
|- ( F e. ( S NMHom T ) -> F e. ( S NGHom T ) ) |
14 |
13
|
adantr |
|- ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> F e. ( S NGHom T ) ) |
15 |
|
nmhmnghm |
|- ( G e. ( S NMHom T ) -> G e. ( S NGHom T ) ) |
16 |
15
|
adantl |
|- ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> G e. ( S NGHom T ) ) |
17 |
1
|
nghmplusg |
|- ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( F oF .+ G ) e. ( S NGHom T ) ) |
18 |
12 14 16 17
|
syl3anc |
|- ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( F oF .+ G ) e. ( S NGHom T ) ) |
19 |
8 18
|
jca |
|- ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( ( F oF .+ G ) e. ( S LMHom T ) /\ ( F oF .+ G ) e. ( S NGHom T ) ) ) |
20 |
|
isnmhm |
|- ( ( F oF .+ G ) e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( ( F oF .+ G ) e. ( S LMHom T ) /\ ( F oF .+ G ) e. ( S NGHom T ) ) ) ) |
21 |
4 19 20
|
sylanbrc |
|- ( ( F e. ( S NMHom T ) /\ G e. ( S NMHom T ) ) -> ( F oF .+ G ) e. ( S NMHom T ) ) |