Metamath Proof Explorer

Theorem nmoid

Description: The operator norm of the identity function on a nontrivial group. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypotheses nmoid.1 
|- N = ( S normOp S )
nmoid.2 
|- V = ( Base ` S )
nmoid.3 
|- .0. = ( 0g ` S )
Assertion nmoid 
|- ( ( S e. NrmGrp /\ { .0. } C. V ) -> ( N ` ( _I |` V ) ) = 1 )

Proof

Step Hyp Ref Expression
1 nmoid.1 
 |-  N = ( S normOp S )
2 nmoid.2 
 |-  V = ( Base ` S )
3 nmoid.3 
 |-  .0. = ( 0g ` S )
4 eqid 
 |-  ( norm ` S ) = ( norm ` S )
5 simpl 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> S e. NrmGrp )
6 ngpgrp 
 |-  ( S e. NrmGrp -> S e. Grp )
7 6 adantr 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> S e. Grp )
8 2 idghm 
 |-  ( S e. Grp -> ( _I |` V ) e. ( S GrpHom S ) )
9 7 8 syl 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> ( _I |` V ) e. ( S GrpHom S ) )
10 1red 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> 1 e. RR )
11 0le1 
 |-  0 <_ 1
12 11 a1i 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> 0 <_ 1 )
13 2 4 nmcl 
 |-  ( ( S e. NrmGrp /\ x e. V ) -> ( ( norm ` S ) ` x ) e. RR )
14 13 ad2ant2r 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( norm ` S ) ` x ) e. RR )
15 14 leidd 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( norm ` S ) ` x ) <_ ( ( norm ` S ) ` x ) )
16 fvresi 
 |-  ( x e. V -> ( ( _I |` V ) ` x ) = x )
17 16 ad2antrl 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( _I |` V ) ` x ) = x )
18 17 fveq2d 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( norm ` S ) ` ( ( _I |` V ) ` x ) ) = ( ( norm ` S ) ` x ) )
19 14 recnd 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( norm ` S ) ` x ) e. CC )
20 19 mulid2d 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( 1 x. ( ( norm ` S ) ` x ) ) = ( ( norm ` S ) ` x ) )
21 15 18 20 3brtr4d 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( norm ` S ) ` ( ( _I |` V ) ` x ) ) <_ ( 1 x. ( ( norm ` S ) ` x ) ) )
22 1 2 4 4 3 5 5 9 10 12 21 nmolb2d 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> ( N ` ( _I |` V ) ) <_ 1 )
23 pssnel 
 |-  ( { .0. } C. V -> E. x ( x e. V /\ -. x e. { .0. } ) )
24 23 adantl 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> E. x ( x e. V /\ -. x e. { .0. } ) )
25 velsn 
 |-  ( x e. { .0. } <-> x = .0. )
26 25 biimpri 
 |-  ( x = .0. -> x e. { .0. } )
27 26 necon3bi 
 |-  ( -. x e. { .0. } -> x =/= .0. )
28 20 18 eqtr4d 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( 1 x. ( ( norm ` S ) ` x ) ) = ( ( norm ` S ) ` ( ( _I |` V ) ` x ) ) )
29 1 nmocl 
 |-  ( ( S e. NrmGrp /\ S e. NrmGrp /\ ( _I |` V ) e. ( S GrpHom S ) ) -> ( N ` ( _I |` V ) ) e. RR* )
30 5 5 9 29 syl3anc 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> ( N ` ( _I |` V ) ) e. RR* )
31 1 nmoge0 
 |-  ( ( S e. NrmGrp /\ S e. NrmGrp /\ ( _I |` V ) e. ( S GrpHom S ) ) -> 0 <_ ( N ` ( _I |` V ) ) )
32 5 5 9 31 syl3anc 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> 0 <_ ( N ` ( _I |` V ) ) )
33 xrrege0 
 |-  ( ( ( ( N ` ( _I |` V ) ) e. RR* /\ 1 e. RR ) /\ ( 0 <_ ( N ` ( _I |` V ) ) /\ ( N ` ( _I |` V ) ) <_ 1 ) ) -> ( N ` ( _I |` V ) ) e. RR )
34 30 10 32 22 33 syl22anc 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> ( N ` ( _I |` V ) ) e. RR )
35 1 isnghm2 
 |-  ( ( S e. NrmGrp /\ S e. NrmGrp /\ ( _I |` V ) e. ( S GrpHom S ) ) -> ( ( _I |` V ) e. ( S NGHom S ) <-> ( N ` ( _I |` V ) ) e. RR ) )
36 5 5 9 35 syl3anc 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> ( ( _I |` V ) e. ( S NGHom S ) <-> ( N ` ( _I |` V ) ) e. RR ) )
37 34 36 mpbird 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> ( _I |` V ) e. ( S NGHom S ) )
38 simprl 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> x e. V )
39 1 2 4 4 nmoi 
 |-  ( ( ( _I |` V ) e. ( S NGHom S ) /\ x e. V ) -> ( ( norm ` S ) ` ( ( _I |` V ) ` x ) ) <_ ( ( N ` ( _I |` V ) ) x. ( ( norm ` S ) ` x ) ) )
40 37 38 39 syl2an2r 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( norm ` S ) ` ( ( _I |` V ) ` x ) ) <_ ( ( N ` ( _I |` V ) ) x. ( ( norm ` S ) ` x ) ) )
41 28 40 eqbrtrd 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( 1 x. ( ( norm ` S ) ` x ) ) <_ ( ( N ` ( _I |` V ) ) x. ( ( norm ` S ) ` x ) ) )
42 1red 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> 1 e. RR )
43 34 adantr 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( N ` ( _I |` V ) ) e. RR )
44 2 4 3 nmrpcl 
 |-  ( ( S e. NrmGrp /\ x e. V /\ x =/= .0. ) -> ( ( norm ` S ) ` x ) e. RR+ )
45 44 3expb 
 |-  ( ( S e. NrmGrp /\ ( x e. V /\ x =/= .0. ) ) -> ( ( norm ` S ) ` x ) e. RR+ )
46 45 adantlr 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( ( norm ` S ) ` x ) e. RR+ )
47 42 43 46 lemul1d 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> ( 1 <_ ( N ` ( _I |` V ) ) <-> ( 1 x. ( ( norm ` S ) ` x ) ) <_ ( ( N ` ( _I |` V ) ) x. ( ( norm ` S ) ` x ) ) ) )
48 41 47 mpbird 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ x =/= .0. ) ) -> 1 <_ ( N ` ( _I |` V ) ) )
49 27 48 sylanr2 
 |-  ( ( ( S e. NrmGrp /\ { .0. } C. V ) /\ ( x e. V /\ -. x e. { .0. } ) ) -> 1 <_ ( N ` ( _I |` V ) ) )
50 24 49 exlimddv 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> 1 <_ ( N ` ( _I |` V ) ) )
51 1xr 
 |-  1 e. RR*
52 xrletri3 
 |-  ( ( ( N ` ( _I |` V ) ) e. RR* /\ 1 e. RR* ) -> ( ( N ` ( _I |` V ) ) = 1 <-> ( ( N ` ( _I |` V ) ) <_ 1 /\ 1 <_ ( N ` ( _I |` V ) ) ) ) )
53 30 51 52 sylancl 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> ( ( N ` ( _I |` V ) ) = 1 <-> ( ( N ` ( _I |` V ) ) <_ 1 /\ 1 <_ ( N ` ( _I |` V ) ) ) ) )
54 22 50 53 mpbir2and 
 |-  ( ( S e. NrmGrp /\ { .0. } C. V ) -> ( N ` ( _I |` V ) ) = 1 )