Step |
Hyp |
Ref |
Expression |
1 |
|
nmhmrcl2 |
|- ( F e. ( T NMHom U ) -> U e. NrmMod ) |
2 |
|
nmhmrcl1 |
|- ( G e. ( S NMHom T ) -> S e. NrmMod ) |
3 |
1 2
|
anim12ci |
|- ( ( F e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( S e. NrmMod /\ U e. NrmMod ) ) |
4 |
|
nmhmlmhm |
|- ( F e. ( T NMHom U ) -> F e. ( T LMHom U ) ) |
5 |
|
nmhmlmhm |
|- ( G e. ( S NMHom T ) -> G e. ( S LMHom T ) ) |
6 |
|
lmhmco |
|- ( ( F e. ( T LMHom U ) /\ G e. ( S LMHom T ) ) -> ( F o. G ) e. ( S LMHom U ) ) |
7 |
4 5 6
|
syl2an |
|- ( ( F e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( F o. G ) e. ( S LMHom U ) ) |
8 |
|
nmhmnghm |
|- ( F e. ( T NMHom U ) -> F e. ( T NGHom U ) ) |
9 |
|
nmhmnghm |
|- ( G e. ( S NMHom T ) -> G e. ( S NGHom T ) ) |
10 |
|
nghmco |
|- ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( F o. G ) e. ( S NGHom U ) ) |
11 |
8 9 10
|
syl2an |
|- ( ( F e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( F o. G ) e. ( S NGHom U ) ) |
12 |
7 11
|
jca |
|- ( ( F e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( ( F o. G ) e. ( S LMHom U ) /\ ( F o. G ) e. ( S NGHom U ) ) ) |
13 |
|
isnmhm |
|- ( ( F o. G ) e. ( S NMHom U ) <-> ( ( S e. NrmMod /\ U e. NrmMod ) /\ ( ( F o. G ) e. ( S LMHom U ) /\ ( F o. G ) e. ( S NGHom U ) ) ) ) |
14 |
3 12 13
|
sylanbrc |
|- ( ( F e. ( T NMHom U ) /\ G e. ( S NMHom T ) ) -> ( F o. G ) e. ( S NMHom U ) ) |