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 ⊢ 𝑁 = ( 𝑆 normOp 𝑆 )
nmoid.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
nmoid.3 ⊢ 0 = ( 0g ‘ 𝑆 )
Assertion nmoid ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → ( 𝑁 ‘ ( I ↾ 𝑉 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 nmoid.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑆 )
2 nmoid.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
3 nmoid.3 ⊢ 0 = ( 0g ‘ 𝑆 )
4 eqid ⊢ ( norm ‘ 𝑆 ) = ( norm ‘ 𝑆 )
5 simpl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → 𝑆 ∈ NrmGrp )
6 ngpgrp ⊢ ( 𝑆 ∈ NrmGrp → 𝑆 ∈ Grp )
7 6 adantr ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → 𝑆 ∈ Grp )
8 2 idghm ⊢ ( 𝑆 ∈ Grp → ( I ↾ 𝑉 ) ∈ ( 𝑆 GrpHom 𝑆 ) )
9 7 8 syl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → ( I ↾ 𝑉 ) ∈ ( 𝑆 GrpHom 𝑆 ) )
10 1red ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → 1 ∈ ℝ )
11 0le1 ⊢ 0 ≤ 1
12 11 a1i ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → 0 ≤ 1 )
13 2 4 nmcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ )
14 13 ad2ant2r ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ )
15 14 leidd ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ≤ ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) )
16 fvresi ⊢ ( 𝑥 ∈ 𝑉 → ( ( I ↾ 𝑉 ) ‘ 𝑥 ) = 𝑥 )
17 16 ad2antrl ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( I ↾ 𝑉 ) ‘ 𝑥 ) = 𝑥 )
18 17 fveq2d ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( norm ‘ 𝑆 ) ‘ ( ( I ↾ 𝑉 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) )
19 14 recnd ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℂ )
20 19 mulid2d ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 1 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) )
21 15 18 20 3brtr4d ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( norm ‘ 𝑆 ) ‘ ( ( I ↾ 𝑉 ) ‘ 𝑥 ) ) ≤ ( 1 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
22 1 2 4 4 3 5 5 9 10 12 21 nmolb2d ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ≤ 1 )
23 pssnel ⊢ ( { 0 } ⊊ 𝑉 → ∃ 𝑥 ( 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ { 0 } ) )
24 23 adantl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → ∃ 𝑥 ( 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ { 0 } ) )
25 velsn ⊢ ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
26 25 biimpri ⊢ ( 𝑥 = 0 → 𝑥 ∈ { 0 } )
27 26 necon3bi ⊢ ( ¬ 𝑥 ∈ { 0 } → 𝑥 ≠ 0 )
28 20 18 eqtr4d ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 1 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑆 ) ‘ ( ( I ↾ 𝑉 ) ‘ 𝑥 ) ) )
29 1 nmocl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑆 ∈ NrmGrp ∧ ( I ↾ 𝑉 ) ∈ ( 𝑆 GrpHom 𝑆 ) ) → ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ∈ ℝ* )
30 5 5 9 29 syl3anc ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ∈ ℝ* )
31 1 nmoge0 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑆 ∈ NrmGrp ∧ ( I ↾ 𝑉 ) ∈ ( 𝑆 GrpHom 𝑆 ) ) → 0 ≤ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) )
32 5 5 9 31 syl3anc ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → 0 ≤ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) )
33 xrrege0 ⊢ ( ( ( ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ∈ ℝ* ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ∧ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ≤ 1 ) ) → ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ∈ ℝ )
34 30 10 32 22 33 syl22anc ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ∈ ℝ )
35 1 isnghm2 ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑆 ∈ NrmGrp ∧ ( I ↾ 𝑉 ) ∈ ( 𝑆 GrpHom 𝑆 ) ) → ( ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) ↔ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ∈ ℝ ) )
36 5 5 9 35 syl3anc ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → ( ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) ↔ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ∈ ℝ ) )
37 34 36 mpbird ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) )
38 simprl ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → 𝑥 ∈ 𝑉 )
39 1 2 4 4 nmoi ⊢ ( ( ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( norm ‘ 𝑆 ) ‘ ( ( I ↾ 𝑉 ) ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ ( I ↾ 𝑉 ) ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
40 37 38 39 syl2an2r ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( norm ‘ 𝑆 ) ‘ ( ( I ↾ 𝑉 ) ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ ( I ↾ 𝑉 ) ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
41 28 40 eqbrtrd ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 1 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ ( I ↾ 𝑉 ) ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
42 1red ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → 1 ∈ ℝ )
43 34 adantr ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ∈ ℝ )
44 2 4 3 nmrpcl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ+ )
45 44 3expb ⊢ ( ( 𝑆 ∈ NrmGrp ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ+ )
46 45 adantlr ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ+ )
47 42 43 46 lemul1d ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 1 ≤ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ↔ ( 1 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ ( I ↾ 𝑉 ) ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ) )
48 41 47 mpbird ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → 1 ≤ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) )
49 27 48 sylanr2 ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ { 0 } ) ) → 1 ≤ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) )
50 24 49 exlimddv ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → 1 ≤ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) )
51 1xr ⊢ 1 ∈ ℝ*
52 xrletri3 ⊢ ( ( ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( 𝑁 ‘ ( I ↾ 𝑉 ) ) = 1 ↔ ( ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ≤ 1 ∧ 1 ≤ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ) ) )
53 30 51 52 sylancl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → ( ( 𝑁 ‘ ( I ↾ 𝑉 ) ) = 1 ↔ ( ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ≤ 1 ∧ 1 ≤ ( 𝑁 ‘ ( I ↾ 𝑉 ) ) ) ) )
54 22 50 53 mpbir2and ⊢ ( ( 𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉 ) → ( 𝑁 ‘ ( I ↾ 𝑉 ) ) = 1 )