nmoi2

Description: The operator norm is a bound on the growth of a vector under the action of the operator. (Contributed by Mario Carneiro, 19-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)$
	nmoi2.z	$⊢ \underset{˙}{0} = 0_{S}$
Assertion	nmoi2	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to \frac{M (F (X))}{L (X)} \leq N (F)$

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		nmoi2.z	$⊢ \underset{˙}{0} = 0_{S}$
6		simpl2	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to T \in NrmGrp$
7		simpl3	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to F \in (S GrpHom T)$
8		eqid	$⊢ {Base}_{T} = {Base}_{T}$
9	2 8	ghmf	$⊢ F \in (S GrpHom T) \to F : V ⟶ {Base}_{T}$
10	7 9	syl	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to F : V ⟶ {Base}_{T}$
11		simprl	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to X \in V$
12	10 11	ffvelrnd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to F (X) \in {Base}_{T}$
13	8 4	nmcl	$⊢ (T \in NrmGrp \land F (X) \in {Base}_{T}) \to M (F (X)) \in ℝ$
14	6 12 13	syl2anc	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to M (F (X)) \in ℝ$
15	14	rexrd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to M (F (X)) \in ℝ^{*}$
16	1	nmocl	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) \in ℝ^{*}$
17	16	adantr	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to N (F) \in ℝ^{*}$
18	2 3 5	nmrpcl	$⊢ (S \in NrmGrp \land X \in V \land X \neq \underset{˙}{0}) \to L (X) \in ℝ^{+}$
19	18	3expb	$⊢ (S \in NrmGrp \land (X \in V \land X \neq \underset{˙}{0})) \to L (X) \in ℝ^{+}$
20	19	3ad2antl1	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to L (X) \in ℝ^{+}$
21	20	rpxrd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to L (X) \in ℝ^{*}$
22	17 21	xmulcld	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to N (F) \cdot_{𝑒} L (X) \in ℝ^{*}$
23	20	rpreccld	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to \frac{1}{L (X)} \in ℝ^{+}$
24	23	rpxrd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to \frac{1}{L (X)} \in ℝ^{*}$
25	23	rpge0d	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to 0 \leq \frac{1}{L (X)}$
26	24 25	jca	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to (\frac{1}{L (X)} \in ℝ^{*} \land 0 \leq \frac{1}{L (X)})$
27	1 2 3 4	nmoix	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to M (F (X)) \leq N (F) \cdot_{𝑒} L (X)$
28	27	adantrr	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to M (F (X)) \leq N (F) \cdot_{𝑒} L (X)$
29		xlemul1a	$⊢ ((M (F (X)) \in ℝ^{} \land N (F) \cdot_{𝑒} L (X) \in ℝ^{} \land (\frac{1}{L (X)} \in ℝ^{*} \land 0 \leq \frac{1}{L (X)})) \land M (F (X)) \leq N (F) \cdot_{𝑒} L (X)) \to M (F (X)) \cdot_{𝑒} (\frac{1}{L (X)}) \leq (N (F) \cdot_{𝑒} L (X)) \cdot_{𝑒} (\frac{1}{L (X)})$
30	15 22 26 28 29	syl31anc	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to M (F (X)) \cdot_{𝑒} (\frac{1}{L (X)}) \leq (N (F) \cdot_{𝑒} L (X)) \cdot_{𝑒} (\frac{1}{L (X)})$
31	23	rpred	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to \frac{1}{L (X)} \in ℝ$
32		rexmul	$⊢ (M (F (X)) \in ℝ \land \frac{1}{L (X)} \in ℝ) \to M (F (X)) \cdot_{𝑒} (\frac{1}{L (X)}) = M (F (X)) (\frac{1}{L (X)})$
33	14 31 32	syl2anc	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to M (F (X)) \cdot_{𝑒} (\frac{1}{L (X)}) = M (F (X)) (\frac{1}{L (X)})$
34	14	recnd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to M (F (X)) \in ℂ$
35	20	rpcnd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to L (X) \in ℂ$
36	20	rpne0d	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to L (X) \neq 0$
37	34 35 36	divrecd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to \frac{M (F (X))}{L (X)} = M (F (X)) (\frac{1}{L (X)})$
38	33 37	eqtr4d	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to M (F (X)) \cdot_{𝑒} (\frac{1}{L (X)}) = \frac{M (F (X))}{L (X)}$
39		xmulass	$⊢ (N (F) \in ℝ^{} \land L (X) \in ℝ^{} \land \frac{1}{L (X)} \in ℝ^{*}) \to (N (F) \cdot_{𝑒} L (X)) \cdot_{𝑒} (\frac{1}{L (X)}) = N (F) \cdot_{𝑒} (L (X) \cdot_{𝑒} (\frac{1}{L (X)}))$
40	17 21 24 39	syl3anc	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to (N (F) \cdot_{𝑒} L (X)) \cdot_{𝑒} (\frac{1}{L (X)}) = N (F) \cdot_{𝑒} (L (X) \cdot_{𝑒} (\frac{1}{L (X)}))$
41	20	rpred	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to L (X) \in ℝ$
42		rexmul	$⊢ (L (X) \in ℝ \land \frac{1}{L (X)} \in ℝ) \to L (X) \cdot_{𝑒} (\frac{1}{L (X)}) = L (X) (\frac{1}{L (X)})$
43	41 31 42	syl2anc	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to L (X) \cdot_{𝑒} (\frac{1}{L (X)}) = L (X) (\frac{1}{L (X)})$
44	35 36	recidd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to L (X) (\frac{1}{L (X)}) = 1$
45	43 44	eqtrd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to L (X) \cdot_{𝑒} (\frac{1}{L (X)}) = 1$
46	45	oveq2d	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to N (F) \cdot_{𝑒} (L (X) \cdot_{𝑒} (\frac{1}{L (X)})) = N (F) \cdot_{𝑒} 1$
47		xmulid1	$⊢ N (F) \in ℝ^{*} \to N (F) \cdot_{𝑒} 1 = N (F)$
48	17 47	syl	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to N (F) \cdot_{𝑒} 1 = N (F)$
49	40 46 48	3eqtrd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to (N (F) \cdot_{𝑒} L (X)) \cdot_{𝑒} (\frac{1}{L (X)}) = N (F)$
50	30 38 49	3brtr3d	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land (X \in V \land X \neq \underset{˙}{0})) \to \frac{M (F (X))}{L (X)} \leq N (F)$

Metamath Proof Explorer

Theorem nmoi2

Proof