Metamath Proof Explorer

Theorem nghmco

Description: The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Assertion nghmco 
|- ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( F o. G ) e. ( S NGHom U ) )

Proof

Step Hyp Ref Expression
1 nghmrcl1 
 |-  ( G e. ( S NGHom T ) -> S e. NrmGrp )
2 1 adantl 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> S e. NrmGrp )
3 nghmrcl2 
 |-  ( F e. ( T NGHom U ) -> U e. NrmGrp )
4 3 adantr 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> U e. NrmGrp )
5 nghmghm 
 |-  ( F e. ( T NGHom U ) -> F e. ( T GrpHom U ) )
6 nghmghm 
 |-  ( G e. ( S NGHom T ) -> G e. ( S GrpHom T ) )
7 ghmco 
 |-  ( ( F e. ( T GrpHom U ) /\ G e. ( S GrpHom T ) ) -> ( F o. G ) e. ( S GrpHom U ) )
8 5 6 7 syl2an 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( F o. G ) e. ( S GrpHom U ) )
9 eqid 
 |-  ( T normOp U ) = ( T normOp U )
10 9 nghmcl 
 |-  ( F e. ( T NGHom U ) -> ( ( T normOp U ) ` F ) e. RR )
11 eqid 
 |-  ( S normOp T ) = ( S normOp T )
12 11 nghmcl 
 |-  ( G e. ( S NGHom T ) -> ( ( S normOp T ) ` G ) e. RR )
13 remulcl 
 |-  ( ( ( ( T normOp U ) ` F ) e. RR /\ ( ( S normOp T ) ` G ) e. RR ) -> ( ( ( T normOp U ) ` F ) x. ( ( S normOp T ) ` G ) ) e. RR )
14 10 12 13 syl2an 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( ( ( T normOp U ) ` F ) x. ( ( S normOp T ) ` G ) ) e. RR )
15 eqid 
 |-  ( S normOp U ) = ( S normOp U )
16 15 9 11 nmoco 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( ( S normOp U ) ` ( F o. G ) ) <_ ( ( ( T normOp U ) ` F ) x. ( ( S normOp T ) ` G ) ) )
17 15 bddnghm 
 |-  ( ( ( S e. NrmGrp /\ U e. NrmGrp /\ ( F o. G ) e. ( S GrpHom U ) ) /\ ( ( ( ( T normOp U ) ` F ) x. ( ( S normOp T ) ` G ) ) e. RR /\ ( ( S normOp U ) ` ( F o. G ) ) <_ ( ( ( T normOp U ) ` F ) x. ( ( S normOp T ) ` G ) ) ) ) -> ( F o. G ) e. ( S NGHom U ) )
18 2 4 8 14 16 17 syl32anc 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( F o. G ) e. ( S NGHom U ) )