Metamath Proof Explorer

Theorem nmoix

Description: The operator norm is a bound on the size of an operator, even when it is infinite (using extended real multiplication). (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 nmoix 
|- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) *e ( 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 1 isnghm2 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) e. RR ) )
6 5 biimpar 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) e. RR ) -> F e. ( S NGHom T ) )
7 1 2 3 4 nmoi 
 |-  ( ( F e. ( S NGHom T ) /\ X e. V ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) x. ( L ` X ) ) )
8 6 7 sylan 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) e. RR ) /\ X e. V ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) x. ( L ` X ) ) )
9 8 an32s 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ ( N ` F ) e. RR ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) x. ( L ` X ) ) )
10 id 
 |-  ( ( N ` F ) e. RR -> ( N ` F ) e. RR )
11 2 3 nmcl 
 |-  ( ( S e. NrmGrp /\ X e. V ) -> ( L ` X ) e. RR )
12 11 3ad2antl1 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( L ` X ) e. RR )
13 rexmul 
 |-  ( ( ( N ` F ) e. RR /\ ( L ` X ) e. RR ) -> ( ( N ` F ) *e ( L ` X ) ) = ( ( N ` F ) x. ( L ` X ) ) )
14 10 12 13 syl2anr 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ ( N ` F ) e. RR ) -> ( ( N ` F ) *e ( L ` X ) ) = ( ( N ` F ) x. ( L ` X ) ) )
15 9 14 breqtrrd 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ ( N ` F ) e. RR ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) *e ( L ` X ) ) )
16 fveq2 
 |-  ( X = ( 0g ` S ) -> ( F ` X ) = ( F ` ( 0g ` S ) ) )
17 16 fveq2d 
 |-  ( X = ( 0g ` S ) -> ( M ` ( F ` X ) ) = ( M ` ( F ` ( 0g ` S ) ) ) )
18 fveq2 
 |-  ( X = ( 0g ` S ) -> ( L ` X ) = ( L ` ( 0g ` S ) ) )
19 18 oveq2d 
 |-  ( X = ( 0g ` S ) -> ( +oo *e ( L ` X ) ) = ( +oo *e ( L ` ( 0g ` S ) ) ) )
20 17 19 breq12d 
 |-  ( X = ( 0g ` S ) -> ( ( M ` ( F ` X ) ) <_ ( +oo *e ( L ` X ) ) <-> ( M ` ( F ` ( 0g ` S ) ) ) <_ ( +oo *e ( L ` ( 0g ` S ) ) ) ) )
21 simpl2 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> T e. NrmGrp )
22 eqid 
 |-  ( Base ` T ) = ( Base ` T )
23 2 22 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : V --> ( Base ` T ) )
24 23 ffvelcdmda 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. V ) -> ( F ` X ) e. ( Base ` T ) )
25 24 3ad2antl3 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( F ` X ) e. ( Base ` T ) )
26 22 4 nmcl 
 |-  ( ( T e. NrmGrp /\ ( F ` X ) e. ( Base ` T ) ) -> ( M ` ( F ` X ) ) e. RR )
27 21 25 26 syl2anc 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( M ` ( F ` X ) ) e. RR )
28 27 adantr 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( M ` ( F ` X ) ) e. RR )
29 28 rexrd 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( M ` ( F ` X ) ) e. RR* )
30 pnfge 
 |-  ( ( M ` ( F ` X ) ) e. RR* -> ( M ` ( F ` X ) ) <_ +oo )
31 29 30 syl 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( M ` ( F ` X ) ) <_ +oo )
32 simp1 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> S e. NrmGrp )
33 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
34 2 3 33 nmrpcl 
 |-  ( ( S e. NrmGrp /\ X e. V /\ X =/= ( 0g ` S ) ) -> ( L ` X ) e. RR+ )
35 34 3expa 
 |-  ( ( ( S e. NrmGrp /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( L ` X ) e. RR+ )
36 32 35 sylanl1 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( L ` X ) e. RR+ )
37 rpxr 
 |-  ( ( L ` X ) e. RR+ -> ( L ` X ) e. RR* )
38 rpgt0 
 |-  ( ( L ` X ) e. RR+ -> 0 < ( L ` X ) )
39 xmulpnf2 
 |-  ( ( ( L ` X ) e. RR* /\ 0 < ( L ` X ) ) -> ( +oo *e ( L ` X ) ) = +oo )
40 37 38 39 syl2anc 
 |-  ( ( L ` X ) e. RR+ -> ( +oo *e ( L ` X ) ) = +oo )
41 36 40 syl 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( +oo *e ( L ` X ) ) = +oo )
42 31 41 breqtrrd 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ X =/= ( 0g ` S ) ) -> ( M ` ( F ` X ) ) <_ ( +oo *e ( L ` X ) ) )
43 0le0 
 |-  0 <_ 0
44 simpl3 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> F e. ( S GrpHom T ) )
45 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
46 33 45 ghmid 
 |-  ( F e. ( S GrpHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
47 44 46 syl 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
48 47 fveq2d 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( M ` ( F ` ( 0g ` S ) ) ) = ( M ` ( 0g ` T ) ) )
49 4 45 nm0 
 |-  ( T e. NrmGrp -> ( M ` ( 0g ` T ) ) = 0 )
50 21 49 syl 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( M ` ( 0g ` T ) ) = 0 )
51 48 50 eqtrd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( M ` ( F ` ( 0g ` S ) ) ) = 0 )
52 simpl1 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> S e. NrmGrp )
53 3 33 nm0 
 |-  ( S e. NrmGrp -> ( L ` ( 0g ` S ) ) = 0 )
54 52 53 syl 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( L ` ( 0g ` S ) ) = 0 )
55 54 oveq2d 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( +oo *e ( L ` ( 0g ` S ) ) ) = ( +oo *e 0 ) )
56 pnfxr 
 |-  +oo e. RR*
57 xmul01 
 |-  ( +oo e. RR* -> ( +oo *e 0 ) = 0 )
58 56 57 ax-mp 
 |-  ( +oo *e 0 ) = 0
59 55 58 eqtrdi 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( +oo *e ( L ` ( 0g ` S ) ) ) = 0 )
60 51 59 breq12d 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( ( M ` ( F ` ( 0g ` S ) ) ) <_ ( +oo *e ( L ` ( 0g ` S ) ) ) <-> 0 <_ 0 ) )
61 43 60 mpbiri 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( M ` ( F ` ( 0g ` S ) ) ) <_ ( +oo *e ( L ` ( 0g ` S ) ) ) )
62 20 42 61 pm2.61ne 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( M ` ( F ` X ) ) <_ ( +oo *e ( L ` X ) ) )
63 62 adantr 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ ( N ` F ) = +oo ) -> ( M ` ( F ` X ) ) <_ ( +oo *e ( L ` X ) ) )
64 simpr 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ ( N ` F ) = +oo ) -> ( N ` F ) = +oo )
65 64 oveq1d 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ ( N ` F ) = +oo ) -> ( ( N ` F ) *e ( L ` X ) ) = ( +oo *e ( L ` X ) ) )
66 63 65 breqtrrd 
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) /\ ( N ` F ) = +oo ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) *e ( L ` X ) ) )
67 1 nmocl 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )
68 1 nmoge0 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> 0 <_ ( N ` F ) )
69 ge0nemnf 
 |-  ( ( ( N ` F ) e. RR* /\ 0 <_ ( N ` F ) ) -> ( N ` F ) =/= -oo )
70 67 68 69 syl2anc 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) =/= -oo )
71 67 70 jca 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( N ` F ) e. RR* /\ ( N ` F ) =/= -oo ) )
72 xrnemnf 
 |-  ( ( ( N ` F ) e. RR* /\ ( N ` F ) =/= -oo ) <-> ( ( N ` F ) e. RR \/ ( N ` F ) = +oo ) )
73 71 72 sylib 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( N ` F ) e. RR \/ ( N ` F ) = +oo ) )
74 73 adantr 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( ( N ` F ) e. RR \/ ( N ` F ) = +oo ) )
75 15 66 74 mpjaodan 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) *e ( L ` X ) ) )