Metamath Proof Explorer

Theorem nmoco

Description: An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypotheses nmoco.1 
|- N = ( S normOp U )
nmoco.2 
|- L = ( T normOp U )
nmoco.3 
|- M = ( S normOp T )
Assertion nmoco 
|- ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( N ` ( F o. G ) ) <_ ( ( L ` F ) x. ( M ` G ) ) )

Proof

Step Hyp Ref Expression
1 nmoco.1 
 |-  N = ( S normOp U )
2 nmoco.2 
 |-  L = ( T normOp U )
3 nmoco.3 
 |-  M = ( S normOp T )
4 eqid 
 |-  ( Base ` S ) = ( Base ` S )
5 eqid 
 |-  ( norm ` S ) = ( norm ` S )
6 eqid 
 |-  ( norm ` U ) = ( norm ` U )
7 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
8 nghmrcl1 
 |-  ( G e. ( S NGHom T ) -> S e. NrmGrp )
9 8 adantl 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> S e. NrmGrp )
10 nghmrcl2 
 |-  ( F e. ( T NGHom U ) -> U e. NrmGrp )
11 10 adantr 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> U e. NrmGrp )
12 nghmghm 
 |-  ( F e. ( T NGHom U ) -> F e. ( T GrpHom U ) )
13 nghmghm 
 |-  ( G e. ( S NGHom T ) -> G e. ( S GrpHom T ) )
14 ghmco 
 |-  ( ( F e. ( T GrpHom U ) /\ G e. ( S GrpHom T ) ) -> ( F o. G ) e. ( S GrpHom U ) )
15 12 13 14 syl2an 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( F o. G ) e. ( S GrpHom U ) )
16 2 nghmcl 
 |-  ( F e. ( T NGHom U ) -> ( L ` F ) e. RR )
17 3 nghmcl 
 |-  ( G e. ( S NGHom T ) -> ( M ` G ) e. RR )
18 remulcl 
 |-  ( ( ( L ` F ) e. RR /\ ( M ` G ) e. RR ) -> ( ( L ` F ) x. ( M ` G ) ) e. RR )
19 16 17 18 syl2an 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( ( L ` F ) x. ( M ` G ) ) e. RR )
20 nghmrcl1 
 |-  ( F e. ( T NGHom U ) -> T e. NrmGrp )
21 2 nmoge0 
 |-  ( ( T e. NrmGrp /\ U e. NrmGrp /\ F e. ( T GrpHom U ) ) -> 0 <_ ( L ` F ) )
22 20 10 12 21 syl3anc 
 |-  ( F e. ( T NGHom U ) -> 0 <_ ( L ` F ) )
23 16 22 jca 
 |-  ( F e. ( T NGHom U ) -> ( ( L ` F ) e. RR /\ 0 <_ ( L ` F ) ) )
24 nghmrcl2 
 |-  ( G e. ( S NGHom T ) -> T e. NrmGrp )
25 3 nmoge0 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ G e. ( S GrpHom T ) ) -> 0 <_ ( M ` G ) )
26 8 24 13 25 syl3anc 
 |-  ( G e. ( S NGHom T ) -> 0 <_ ( M ` G ) )
27 17 26 jca 
 |-  ( G e. ( S NGHom T ) -> ( ( M ` G ) e. RR /\ 0 <_ ( M ` G ) ) )
28 mulge0 
 |-  ( ( ( ( L ` F ) e. RR /\ 0 <_ ( L ` F ) ) /\ ( ( M ` G ) e. RR /\ 0 <_ ( M ` G ) ) ) -> 0 <_ ( ( L ` F ) x. ( M ` G ) ) )
29 23 27 28 syl2an 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> 0 <_ ( ( L ` F ) x. ( M ` G ) ) )
30 10 ad2antrr 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> U e. NrmGrp )
31 12 ad2antrr 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> F e. ( T GrpHom U ) )
32 eqid 
 |-  ( Base ` T ) = ( Base ` T )
33 eqid 
 |-  ( Base ` U ) = ( Base ` U )
34 32 33 ghmf 
 |-  ( F e. ( T GrpHom U ) -> F : ( Base ` T ) --> ( Base ` U ) )
35 31 34 syl 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> F : ( Base ` T ) --> ( Base ` U ) )
36 13 ad2antlr 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> G e. ( S GrpHom T ) )
37 4 32 ghmf 
 |-  ( G e. ( S GrpHom T ) -> G : ( Base ` S ) --> ( Base ` T ) )
38 36 37 syl 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> G : ( Base ` S ) --> ( Base ` T ) )
39 simprl 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> x e. ( Base ` S ) )
40 38 39 ffvelrnd 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( G ` x ) e. ( Base ` T ) )
41 35 40 ffvelrnd 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( F ` ( G ` x ) ) e. ( Base ` U ) )
42 33 6 nmcl 
 |-  ( ( U e. NrmGrp /\ ( F ` ( G ` x ) ) e. ( Base ` U ) ) -> ( ( norm ` U ) ` ( F ` ( G ` x ) ) ) e. RR )
43 30 41 42 syl2anc 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` U ) ` ( F ` ( G ` x ) ) ) e. RR )
44 16 ad2antrr 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( L ` F ) e. RR )
45 20 ad2antrr 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> T e. NrmGrp )
46 eqid 
 |-  ( norm ` T ) = ( norm ` T )
47 32 46 nmcl 
 |-  ( ( T e. NrmGrp /\ ( G ` x ) e. ( Base ` T ) ) -> ( ( norm ` T ) ` ( G ` x ) ) e. RR )
48 45 40 47 syl2anc 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` T ) ` ( G ` x ) ) e. RR )
49 44 48 remulcld 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( L ` F ) x. ( ( norm ` T ) ` ( G ` x ) ) ) e. RR )
50 17 ad2antlr 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( M ` G ) e. RR )
51 4 5 nmcl 
 |-  ( ( S e. NrmGrp /\ x e. ( Base ` S ) ) -> ( ( norm ` S ) ` x ) e. RR )
52 8 51 sylan 
 |-  ( ( G e. ( S NGHom T ) /\ x e. ( Base ` S ) ) -> ( ( norm ` S ) ` x ) e. RR )
53 52 ad2ant2lr 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` S ) ` x ) e. RR )
54 50 53 remulcld 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( M ` G ) x. ( ( norm ` S ) ` x ) ) e. RR )
55 44 54 remulcld 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( L ` F ) x. ( ( M ` G ) x. ( ( norm ` S ) ` x ) ) ) e. RR )
56 simpll 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> F e. ( T NGHom U ) )
57 2 32 46 6 nmoi 
 |-  ( ( F e. ( T NGHom U ) /\ ( G ` x ) e. ( Base ` T ) ) -> ( ( norm ` U ) ` ( F ` ( G ` x ) ) ) <_ ( ( L ` F ) x. ( ( norm ` T ) ` ( G ` x ) ) ) )
58 56 40 57 syl2anc 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` U ) ` ( F ` ( G ` x ) ) ) <_ ( ( L ` F ) x. ( ( norm ` T ) ` ( G ` x ) ) ) )
59 23 ad2antrr 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( L ` F ) e. RR /\ 0 <_ ( L ` F ) ) )
60 3 4 5 46 nmoi 
 |-  ( ( G e. ( S NGHom T ) /\ x e. ( Base ` S ) ) -> ( ( norm ` T ) ` ( G ` x ) ) <_ ( ( M ` G ) x. ( ( norm ` S ) ` x ) ) )
61 60 ad2ant2lr 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` T ) ` ( G ` x ) ) <_ ( ( M ` G ) x. ( ( norm ` S ) ` x ) ) )
62 lemul2a 
 |-  ( ( ( ( ( norm ` T ) ` ( G ` x ) ) e. RR /\ ( ( M ` G ) x. ( ( norm ` S ) ` x ) ) e. RR /\ ( ( L ` F ) e. RR /\ 0 <_ ( L ` F ) ) ) /\ ( ( norm ` T ) ` ( G ` x ) ) <_ ( ( M ` G ) x. ( ( norm ` S ) ` x ) ) ) -> ( ( L ` F ) x. ( ( norm ` T ) ` ( G ` x ) ) ) <_ ( ( L ` F ) x. ( ( M ` G ) x. ( ( norm ` S ) ` x ) ) ) )
63 48 54 59 61 62 syl31anc 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( L ` F ) x. ( ( norm ` T ) ` ( G ` x ) ) ) <_ ( ( L ` F ) x. ( ( M ` G ) x. ( ( norm ` S ) ` x ) ) ) )
64 43 49 55 58 63 letrd 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` U ) ` ( F ` ( G ` x ) ) ) <_ ( ( L ` F ) x. ( ( M ` G ) x. ( ( norm ` S ) ` x ) ) ) )
65 fvco3 
 |-  ( ( G : ( Base ` S ) --> ( Base ` T ) /\ x e. ( Base ` S ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
66 38 39 65 syl2anc 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
67 66 fveq2d 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` U ) ` ( ( F o. G ) ` x ) ) = ( ( norm ` U ) ` ( F ` ( G ` x ) ) ) )
68 44 recnd 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( L ` F ) e. CC )
69 50 recnd 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( M ` G ) e. CC )
70 53 recnd 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` S ) ` x ) e. CC )
71 68 69 70 mulassd 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( ( L ` F ) x. ( M ` G ) ) x. ( ( norm ` S ) ` x ) ) = ( ( L ` F ) x. ( ( M ` G ) x. ( ( norm ` S ) ` x ) ) ) )
72 64 67 71 3brtr4d 
 |-  ( ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) /\ ( x e. ( Base ` S ) /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` U ) ` ( ( F o. G ) ` x ) ) <_ ( ( ( L ` F ) x. ( M ` G ) ) x. ( ( norm ` S ) ` x ) ) )
73 1 4 5 6 7 9 11 15 19 29 72 nmolb2d 
 |-  ( ( F e. ( T NGHom U ) /\ G e. ( S NGHom T ) ) -> ( N ` ( F o. G ) ) <_ ( ( L ` F ) x. ( M ` G ) ) )