Metamath Proof Explorer

Theorem nmoi

Description: The operator norm achieves the minimum of the set of upper bounds, if the operator is bounded. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypotheses nmofval.1 
|- N = ( S normOp T )
nmoi.2 
|- V = ( Base ` S )
nmoi.3 
|- L = ( norm ` S )
nmoi.4 
|- M = ( norm ` T )
Assertion nmoi 
|- ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) x. ( L ` X ) ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 
 |-  N = ( S normOp T )
2 nmoi.2 
 |-  V = ( Base ` S )
3 nmoi.3 
 |-  L = ( norm ` S )
4 nmoi.4 
 |-  M = ( norm ` T )
5 2fveq3 
 |-  ( X = ( 0g ` S ) -> ( M ` ( F ` X ) ) = ( M ` ( F ` ( 0g ` S ) ) ) )
6 fveq2 
 |-  ( X = ( 0g ` S ) -> ( L ` X ) = ( L ` ( 0g ` S ) ) )
7 6 oveq2d 
 |-  ( X = ( 0g ` S ) -> ( ( N ` F ) x. ( L ` X ) ) = ( ( N ` F ) x. ( L ` ( 0g ` S ) ) ) )
8 5 7 breq12d 
 |-  ( X = ( 0g ` S ) -> ( ( M ` ( F ` X ) ) <_ ( ( N ` F ) x. ( L ` X ) ) <-> ( M ` ( F ` ( 0g ` S ) ) ) <_ ( ( N ` F ) x. ( L ` ( 0g ` S ) ) ) ) )
9 2fveq3 
 |-  ( x = X -> ( M ` ( F ` x ) ) = ( M ` ( F ` X ) ) )
10 fveq2 
 |-  ( x = X -> ( L ` x ) = ( L ` X ) )
11 10 oveq2d 
 |-  ( x = X -> ( r x. ( L ` x ) ) = ( r x. ( L ` X ) ) )
12 9 11 breq12d 
 |-  ( x = X -> ( ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) <-> ( M ` ( F ` X ) ) <_ ( r x. ( L ` X ) ) ) )
13 12 rspcv 
 |-  ( X e. V -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( M ` ( F ` X ) ) <_ ( r x. ( L ` X ) ) ) )
14 13 ad3antlr 
 |-  ( ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) /\ r e. ( 0 [,) +oo ) ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( M ` ( F ` X ) ) <_ ( r x. ( L ` X ) ) ) )
15 1 isnghm 
 |-  ( F e. ( S NGHom T ) <-> ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )
16 15 simplbi 
 |-  ( F e. ( S NGHom T ) -> ( S e. NrmGrp /\ T e. NrmGrp ) )
17 16 adantr 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( S e. NrmGrp /\ T e. NrmGrp ) )
18 17 simprd 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> T e. NrmGrp )
19 15 simprbi 
 |-  ( F e. ( S NGHom T ) -> ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) )
20 19 adantr 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) )
21 20 simpld 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> F e. ( S GrpHom T ) )
22 eqid 
 |-  ( Base ` T ) = ( Base ` T )
23 2 22 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : V --> ( Base ` T ) )
24 21 23 syl 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> F : V --> ( Base ` T ) )
25 ffvelcdm 
 |-  ( ( F : V --> ( Base ` T ) /\ X e. V ) -> ( F ` X ) e. ( Base ` T ) )
26 24 25 sylancom 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( F ` X ) e. ( Base ` T ) )
27 22 4 nmcl 
 |-  ( ( T e. NrmGrp /\ ( F ` X ) e. ( Base ` T ) ) -> ( M ` ( F ` X ) ) e. RR )
28 18 26 27 syl2anc 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( M ` ( F ` X ) ) e. RR )
29 28 adantr 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( M ` ( F ` X ) ) e. RR )
30 29 adantr 
 |-  ( ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) /\ r e. ( 0 [,) +oo ) ) -> ( M ` ( F ` X ) ) e. RR )
31 elrege0 
 |-  ( r e. ( 0 [,) +oo ) <-> ( r e. RR /\ 0 <_ r ) )
32 31 simplbi 
 |-  ( r e. ( 0 [,) +oo ) -> r e. RR )
33 32 adantl 
 |-  ( ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) /\ r e. ( 0 [,) +oo ) ) -> r e. RR )
34 17 simpld 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> S e. NrmGrp )
35 simpr 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> X e. V )
36 34 35 jca 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( S e. NrmGrp /\ X e. V ) )
37 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
38 2 3 37 nmrpcl 
 |-  ( ( S e. NrmGrp /\ X e. V /\ X =/= ( 0g ` S ) ) -> ( L ` X ) e. RR+ )
39 38 3expa 
 |-  ( ( ( S e. NrmGrp /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( L ` X ) e. RR+ )
40 36 39 sylan 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( L ` X ) e. RR+ )
41 40 rpregt0d 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( ( L ` X ) e. RR /\ 0 < ( L ` X ) ) )
42 41 adantr 
 |-  ( ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) /\ r e. ( 0 [,) +oo ) ) -> ( ( L ` X ) e. RR /\ 0 < ( L ` X ) ) )
43 ledivmul2 
 |-  ( ( ( M ` ( F ` X ) ) e. RR /\ r e. RR /\ ( ( L ` X ) e. RR /\ 0 < ( L ` X ) ) ) -> ( ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ r <-> ( M ` ( F ` X ) ) <_ ( r x. ( L ` X ) ) ) )
44 30 33 42 43 syl3anc 
 |-  ( ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) /\ r e. ( 0 [,) +oo ) ) -> ( ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ r <-> ( M ` ( F ` X ) ) <_ ( r x. ( L ` X ) ) ) )
45 14 44 sylibrd 
 |-  ( ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) /\ r e. ( 0 [,) +oo ) ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ r ) )
46 45 ralrimiva 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ r ) )
47 34 adantr 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> S e. NrmGrp )
48 18 adantr 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> T e. NrmGrp )
49 21 adantr 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> F e. ( S GrpHom T ) )
50 29 40 rerpdivcld 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( ( M ` ( F ` X ) ) / ( L ` X ) ) e. RR )
51 50 rexrd 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( ( M ` ( F ` X ) ) / ( L ` X ) ) e. RR* )
52 1 2 3 4 nmogelb 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( ( M ` ( F ` X ) ) / ( L ` X ) ) e. RR* ) -> ( ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ r ) ) )
53 47 48 49 51 52 syl31anc 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. V ( M ` ( F ` x ) ) <_ ( r x. ( L ` x ) ) -> ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ r ) ) )
54 46 53 mpbird 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ ( N ` F ) )
55 20 simprd 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( N ` F ) e. RR )
56 55 adantr 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( N ` F ) e. RR )
57 29 56 40 ledivmul2d 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ ( N ` F ) <-> ( M ` ( F ` X ) ) <_ ( ( N ` F ) x. ( L ` X ) ) ) )
58 54 57 mpbid 
 |-  ( ( ( F e. ( S NGHom T ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) x. ( L ` X ) ) )
59 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
60 37 59 ghmid 
 |-  ( F e. ( S GrpHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
61 21 60 syl 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
62 61 fveq2d 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( M ` ( F ` ( 0g ` S ) ) ) = ( M ` ( 0g ` T ) ) )
63 4 59 nm0 
 |-  ( T e. NrmGrp -> ( M ` ( 0g ` T ) ) = 0 )
64 18 63 syl 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( M ` ( 0g ` T ) ) = 0 )
65 62 64 eqtrd 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( M ` ( F ` ( 0g ` S ) ) ) = 0 )
66 3 37 nm0 
 |-  ( S e. NrmGrp -> ( L ` ( 0g ` S ) ) = 0 )
67 34 66 syl 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( L ` ( 0g ` S ) ) = 0 )
68 0re 
 |-  0 e. RR
69 67 68 eqeltrdi 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( L ` ( 0g ` S ) ) e. RR )
70 1 nmoge0 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> 0 <_ ( N ` F ) )
71 34 18 21 70 syl3anc 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> 0 <_ ( N ` F ) )
72 0le0 
 |-  0 <_ 0
73 72 67 breqtrrid 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> 0 <_ ( L ` ( 0g ` S ) ) )
74 55 69 71 73 mulge0d 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> 0 <_ ( ( N ` F ) x. ( L ` ( 0g ` S ) ) ) )
75 65 74 eqbrtrd 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( M ` ( F ` ( 0g ` S ) ) ) <_ ( ( N ` F ) x. ( L ` ( 0g ` S ) ) ) )
76 8 58 75 pm2.61ne 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) x. ( L ` X ) ) )