Step |
Hyp |
Ref |
Expression |
1 |
|
ghmmhm |
|- ( F e. ( T GrpHom U ) -> F e. ( T MndHom U ) ) |
2 |
|
ghmmhm |
|- ( G e. ( S GrpHom T ) -> G e. ( S MndHom T ) ) |
3 |
|
mhmco |
|- ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( F o. G ) e. ( S MndHom U ) ) |
4 |
1 2 3
|
syl2an |
|- ( ( F e. ( T GrpHom U ) /\ G e. ( S GrpHom T ) ) -> ( F o. G ) e. ( S MndHom U ) ) |
5 |
|
ghmgrp1 |
|- ( G e. ( S GrpHom T ) -> S e. Grp ) |
6 |
|
ghmgrp2 |
|- ( F e. ( T GrpHom U ) -> U e. Grp ) |
7 |
|
ghmmhmb |
|- ( ( S e. Grp /\ U e. Grp ) -> ( S GrpHom U ) = ( S MndHom U ) ) |
8 |
5 6 7
|
syl2anr |
|- ( ( F e. ( T GrpHom U ) /\ G e. ( S GrpHom T ) ) -> ( S GrpHom U ) = ( S MndHom U ) ) |
9 |
4 8
|
eleqtrrd |
|- ( ( F e. ( T GrpHom U ) /\ G e. ( S GrpHom T ) ) -> ( F o. G ) e. ( S GrpHom U ) ) |