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	$⊢ \underset{˙}{0} = 0_{S}$
Assertion	nmoid	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to 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	$⊢ \underset{˙}{0} = 0_{S}$
4		eqid	$⊢ norm (S) = norm (S)$
5		simpl	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to S \in NrmGrp$
6		ngpgrp	$⊢ S \in NrmGrp \to S \in Grp$
7	6	adantr	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to S \in Grp$
8	2	idghm	$⊢ S \in Grp \to {I ↾}_{V} \in (S GrpHom S)$
9	7 8	syl	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to {I ↾}_{V} \in (S GrpHom S)$
10		1red	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to 1 \in ℝ$
11		0le1	$⊢ 0 \leq 1$
12	11	a1i	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to 0 \leq 1$
13	2 4	nmcl	$⊢ (S \in NrmGrp \land x \in V) \to norm (S) (x) \in ℝ$
14	13	ad2ant2r	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to norm (S) (x) \in ℝ$
15	14	leidd	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to norm (S) (x) \leq norm (S) (x)$
16		fvresi	$⊢ x \in V \to ({I ↾}_{V}) (x) = x$
17	16	ad2antrl	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to ({I ↾}_{V}) (x) = x$
18	17	fveq2d	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to norm (S) (({I ↾}_{V}) (x)) = norm (S) (x)$
19	14	recnd	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to norm (S) (x) \in ℂ$
20	19	mullidd	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to 1 norm (S) (x) = norm (S) (x)$
21	15 18 20	3brtr4d	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to norm (S) (({I ↾}_{V}) (x)) \leq 1 norm (S) (x)$
22	1 2 4 4 3 5 5 9 10 12 21	nmolb2d	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to N ({I ↾}_{V}) \leq 1$
23		pssnel	$⊢ \{\underset{˙}{0}\} \subset V \to \exists x (x \in V \land \neg x \in \{\underset{˙}{0}\})$
24	23	adantl	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to \exists x (x \in V \land \neg x \in \{\underset{˙}{0}\})$
25		velsn	$⊢ x \in \{\underset{˙}{0}\} \leftrightarrow x = \underset{˙}{0}$
26	25	biimpri	$⊢ x = \underset{˙}{0} \to x \in \{\underset{˙}{0}\}$
27	26	necon3bi	$⊢ \neg x \in \{\underset{˙}{0}\} \to x \neq \underset{˙}{0}$
28	20 18	eqtr4d	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to 1 norm (S) (x) = norm (S) (({I ↾}_{V}) (x))$
29	1	nmocl	$⊢ (S \in NrmGrp \land S \in NrmGrp \land {I ↾}_{V} \in (S GrpHom S)) \to N ({I ↾}_{V}) \in ℝ^{*}$
30	5 5 9 29	syl3anc	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to N ({I ↾}_{V}) \in ℝ^{*}$
31	1	nmoge0	$⊢ (S \in NrmGrp \land S \in NrmGrp \land {I ↾}_{V} \in (S GrpHom S)) \to 0 \leq N ({I ↾}_{V})$
32	5 5 9 31	syl3anc	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to 0 \leq N ({I ↾}_{V})$
33		xrrege0	$⊢ ((N ({I ↾}_{V}) \in ℝ^{*} \land 1 \in ℝ) \land (0 \leq N ({I ↾}_{V}) \land N ({I ↾}_{V}) \leq 1)) \to N ({I ↾}_{V}) \in ℝ$
34	30 10 32 22 33	syl22anc	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to N ({I ↾}_{V}) \in ℝ$
35	1	isnghm2	$⊢ (S \in NrmGrp \land S \in NrmGrp \land {I ↾}_{V} \in (S GrpHom S)) \to ({I ↾}_{V} \in (S NGHom S) \leftrightarrow N ({I ↾}_{V}) \in ℝ)$
36	5 5 9 35	syl3anc	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to ({I ↾}_{V} \in (S NGHom S) \leftrightarrow N ({I ↾}_{V}) \in ℝ)$
37	34 36	mpbird	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to {I ↾}_{V} \in (S NGHom S)$
38		simprl	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to x \in V$
39	1 2 4 4	nmoi	$⊢ ({I ↾}_{V} \in (S NGHom S) \land x \in V) \to norm (S) (({I ↾}_{V}) (x)) \leq N ({I ↾}_{V}) norm (S) (x)$
40	37 38 39	syl2an2r	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to norm (S) (({I ↾}_{V}) (x)) \leq N ({I ↾}_{V}) norm (S) (x)$
41	28 40	eqbrtrd	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to 1 norm (S) (x) \leq N ({I ↾}_{V}) norm (S) (x)$
42		1red	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to 1 \in ℝ$
43	34	adantr	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to N ({I ↾}_{V}) \in ℝ$
44	2 4 3	nmrpcl	$⊢ (S \in NrmGrp \land x \in V \land x \neq \underset{˙}{0}) \to norm (S) (x) \in ℝ^{+}$
45	44	3expb	$⊢ (S \in NrmGrp \land (x \in V \land x \neq \underset{˙}{0})) \to norm (S) (x) \in ℝ^{+}$
46	45	adantlr	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to norm (S) (x) \in ℝ^{+}$
47	42 43 46	lemul1d	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to (1 \leq N ({I ↾}_{V}) \leftrightarrow 1 norm (S) (x) \leq N ({I ↾}_{V}) norm (S) (x))$
48	41 47	mpbird	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land x \neq \underset{˙}{0})) \to 1 \leq N ({I ↾}_{V})$
49	27 48	sylanr2	$⊢ ((S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \land (x \in V \land \neg x \in \{\underset{˙}{0}\})) \to 1 \leq N ({I ↾}_{V})$
50	24 49	exlimddv	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to 1 \leq N ({I ↾}_{V})$
51		1xr	$⊢ 1 \in ℝ^{*}$
52		xrletri3	$⊢ (N ({I ↾}_{V}) \in ℝ^{} \land 1 \in ℝ^{}) \to (N ({I ↾}_{V}) = 1 \leftrightarrow (N ({I ↾}_{V}) \leq 1 \land 1 \leq N ({I ↾}_{V})))$
53	30 51 52	sylancl	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to (N ({I ↾}_{V}) = 1 \leftrightarrow (N ({I ↾}_{V}) \leq 1 \land 1 \leq N ({I ↾}_{V})))$
54	22 50 53	mpbir2and	$⊢ (S \in NrmGrp \land \{\underset{˙}{0}\} \subset V) \to N ({I ↾}_{V}) = 1$

Metamath Proof Explorer

Theorem nmoid

Proof