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	mullidd	⊢ ( ( ( 𝑆 ∈ 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 )