nmoix

Description: The operator norm is a bound on the size of an operator, even when it is infinite (using extended real multiplication). (Contributed by Mario Carneiro, 18-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)$
Assertion	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)$

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	1	isnghm2	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (F \in (S NGHom T) \leftrightarrow N (F) \in ℝ)$
6	5	biimpar	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) \in ℝ) \to F \in (S NGHom T)$
7	1 2 3 4	nmoi	$⊢ (F \in (S NGHom T) \land X \in V) \to M (F (X)) \leq N (F) L (X)$
8	6 7	sylan	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) \in ℝ) \land X \in V) \to M (F (X)) \leq N (F) L (X)$
9	8	an32s	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land N (F) \in ℝ) \to M (F (X)) \leq N (F) L (X)$
10		id	$⊢ N (F) \in ℝ \to N (F) \in ℝ$
11	2 3	nmcl	$⊢ (S \in NrmGrp \land X \in V) \to L (X) \in ℝ$
12	11	3ad2antl1	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to L (X) \in ℝ$
13		rexmul	$⊢ (N (F) \in ℝ \land L (X) \in ℝ) \to N (F) \cdot_{𝑒} L (X) = N (F) L (X)$
14	10 12 13	syl2anr	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land N (F) \in ℝ) \to N (F) \cdot_{𝑒} L (X) = N (F) L (X)$
15	9 14	breqtrrd	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land N (F) \in ℝ) \to M (F (X)) \leq N (F) \cdot_{𝑒} L (X)$
16		fveq2	$⊢ X = 0_{S} \to F (X) = F (0_{S})$
17	16	fveq2d	$⊢ X = 0_{S} \to M (F (X)) = M (F (0_{S}))$
18		fveq2	$⊢ X = 0_{S} \to L (X) = L (0_{S})$
19	18	oveq2d	$⊢ X = 0_{S} \to +∞ \cdot_{𝑒} L (X) = +∞ \cdot_{𝑒} L (0_{S})$
20	17 19	breq12d	$⊢ X = 0_{S} \to (M (F (X)) \leq +∞ \cdot_{𝑒} L (X) \leftrightarrow M (F (0_{S})) \leq +∞ \cdot_{𝑒} L (0_{S}))$
21		simpl2	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to T \in NrmGrp$
22		eqid	$⊢ {Base}_{T} = {Base}_{T}$
23	2 22	ghmf	$⊢ F \in (S GrpHom T) \to F : V ⟶ {Base}_{T}$
24	23	ffvelcdmda	$⊢ (F \in (S GrpHom T) \land X \in V) \to F (X) \in {Base}_{T}$
25	24	3ad2antl3	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to F (X) \in {Base}_{T}$
26	22 4	nmcl	$⊢ (T \in NrmGrp \land F (X) \in {Base}_{T}) \to M (F (X)) \in ℝ$
27	21 25 26	syl2anc	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to M (F (X)) \in ℝ$
28	27	adantr	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land X \neq 0_{S}) \to M (F (X)) \in ℝ$
29	28	rexrd	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land X \neq 0_{S}) \to M (F (X)) \in ℝ^{*}$
30		pnfge	$⊢ M (F (X)) \in ℝ^{*} \to M (F (X)) \leq +∞$
31	29 30	syl	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land X \neq 0_{S}) \to M (F (X)) \leq +∞$
32		simp1	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to S \in NrmGrp$
33		eqid	$⊢ 0_{S} = 0_{S}$
34	2 3 33	nmrpcl	$⊢ (S \in NrmGrp \land X \in V \land X \neq 0_{S}) \to L (X) \in ℝ^{+}$
35	34	3expa	$⊢ ((S \in NrmGrp \land X \in V) \land X \neq 0_{S}) \to L (X) \in ℝ^{+}$
36	32 35	sylanl1	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land X \neq 0_{S}) \to L (X) \in ℝ^{+}$
37		rpxr	$⊢ L (X) \in ℝ^{+} \to L (X) \in ℝ^{*}$
38		rpgt0	$⊢ L (X) \in ℝ^{+} \to 0 < L (X)$
39		xmulpnf2	$⊢ (L (X) \in ℝ^{*} \land 0 < L (X)) \to +∞ \cdot_{𝑒} L (X) = +∞$
40	37 38 39	syl2anc	$⊢ L (X) \in ℝ^{+} \to +∞ \cdot_{𝑒} L (X) = +∞$
41	36 40	syl	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land X \neq 0_{S}) \to +∞ \cdot_{𝑒} L (X) = +∞$
42	31 41	breqtrrd	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land X \neq 0_{S}) \to M (F (X)) \leq +∞ \cdot_{𝑒} L (X)$
43		0le0	$⊢ 0 \leq 0$
44		simpl3	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to F \in (S GrpHom T)$
45		eqid	$⊢ 0_{T} = 0_{T}$
46	33 45	ghmid	$⊢ F \in (S GrpHom T) \to F (0_{S}) = 0_{T}$
47	44 46	syl	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to F (0_{S}) = 0_{T}$
48	47	fveq2d	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to M (F (0_{S})) = M (0_{T})$
49	4 45	nm0	$⊢ T \in NrmGrp \to M (0_{T}) = 0$
50	21 49	syl	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to M (0_{T}) = 0$
51	48 50	eqtrd	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to M (F (0_{S})) = 0$
52		simpl1	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to S \in NrmGrp$
53	3 33	nm0	$⊢ S \in NrmGrp \to L (0_{S}) = 0$
54	52 53	syl	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to L (0_{S}) = 0$
55	54	oveq2d	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to +∞ \cdot_{𝑒} L (0_{S}) = +∞ \cdot_{𝑒} 0$
56		pnfxr	$⊢ +∞ \in ℝ^{*}$
57		xmul01	$⊢ +∞ \in ℝ^{*} \to +∞ \cdot_{𝑒} 0 = 0$
58	56 57	ax-mp	$⊢ +∞ \cdot_{𝑒} 0 = 0$
59	55 58	eqtrdi	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to +∞ \cdot_{𝑒} L (0_{S}) = 0$
60	51 59	breq12d	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to (M (F (0_{S})) \leq +∞ \cdot_{𝑒} L (0_{S}) \leftrightarrow 0 \leq 0)$
61	43 60	mpbiri	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to M (F (0_{S})) \leq +∞ \cdot_{𝑒} L (0_{S})$
62	20 42 61	pm2.61ne	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to M (F (X)) \leq +∞ \cdot_{𝑒} L (X)$
63	62	adantr	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land N (F) = +∞) \to M (F (X)) \leq +∞ \cdot_{𝑒} L (X)$
64		simpr	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land N (F) = +∞) \to N (F) = +∞$
65	64	oveq1d	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land N (F) = +∞) \to N (F) \cdot_{𝑒} L (X) = +∞ \cdot_{𝑒} L (X)$
66	63 65	breqtrrd	$⊢ (((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \land N (F) = +∞) \to M (F (X)) \leq N (F) \cdot_{𝑒} L (X)$
67	1	nmocl	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) \in ℝ^{*}$
68	1	nmoge0	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to 0 \leq N (F)$
69		ge0nemnf	$⊢ (N (F) \in ℝ^{*} \land 0 \leq N (F)) \to N (F) \neq −∞$
70	67 68 69	syl2anc	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) \neq −∞$
71	67 70	jca	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (N (F) \in ℝ^{*} \land N (F) \neq −∞)$
72		xrnemnf	$⊢ (N (F) \in ℝ^{*} \land N (F) \neq −∞) \leftrightarrow (N (F) \in ℝ \lor N (F) = +∞)$
73	71 72	sylib	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (N (F) \in ℝ \lor N (F) = +∞)$
74	73	adantr	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land X \in V) \to (N (F) \in ℝ \lor N (F) = +∞)$
75	15 66 74	mpjaodan	$⊢ ((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)$

Metamath Proof Explorer

Theorem nmoix

Proof