nmoco

Description: An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015)

	Ref	Expression
Hypotheses	nmoco.1	$⊢ N = S normOp U$
	nmoco.2	$⊢ L = T normOp U$
	nmoco.3	$⊢ M = S normOp T$
Assertion	nmoco	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to N (F \circ G) \leq L (F) M (G)$

Proof

Step	Hyp	Ref	Expression
1		nmoco.1	$⊢ N = S normOp U$
2		nmoco.2	$⊢ L = T normOp U$
3		nmoco.3	$⊢ M = S normOp T$
4		eqid	$⊢ {Base}_{S} = {Base}_{S}$
5		eqid	$⊢ norm (S) = norm (S)$
6		eqid	$⊢ norm (U) = norm (U)$
7		eqid	$⊢ 0_{S} = 0_{S}$
8		nghmrcl1	$⊢ G \in (S NGHom T) \to S \in NrmGrp$
9	8	adantl	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to S \in NrmGrp$
10		nghmrcl2	$⊢ F \in (T NGHom U) \to U \in NrmGrp$
11	10	adantr	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to U \in NrmGrp$
12		nghmghm	$⊢ F \in (T NGHom U) \to F \in (T GrpHom U)$
13		nghmghm	$⊢ G \in (S NGHom T) \to G \in (S GrpHom T)$
14		ghmco	$⊢ (F \in (T GrpHom U) \land G \in (S GrpHom T)) \to F \circ G \in (S GrpHom U)$
15	12 13 14	syl2an	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to F \circ G \in (S GrpHom U)$
16	2	nghmcl	$⊢ F \in (T NGHom U) \to L (F) \in ℝ$
17	3	nghmcl	$⊢ G \in (S NGHom T) \to M (G) \in ℝ$
18		remulcl	$⊢ (L (F) \in ℝ \land M (G) \in ℝ) \to L (F) M (G) \in ℝ$
19	16 17 18	syl2an	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to L (F) M (G) \in ℝ$
20		nghmrcl1	$⊢ F \in (T NGHom U) \to T \in NrmGrp$
21	2	nmoge0	$⊢ (T \in NrmGrp \land U \in NrmGrp \land F \in (T GrpHom U)) \to 0 \leq L (F)$
22	20 10 12 21	syl3anc	$⊢ F \in (T NGHom U) \to 0 \leq L (F)$
23	16 22	jca	$⊢ F \in (T NGHom U) \to (L (F) \in ℝ \land 0 \leq L (F))$
24		nghmrcl2	$⊢ G \in (S NGHom T) \to T \in NrmGrp$
25	3	nmoge0	$⊢ (S \in NrmGrp \land T \in NrmGrp \land G \in (S GrpHom T)) \to 0 \leq M (G)$
26	8 24 13 25	syl3anc	$⊢ G \in (S NGHom T) \to 0 \leq M (G)$
27	17 26	jca	$⊢ G \in (S NGHom T) \to (M (G) \in ℝ \land 0 \leq M (G))$
28		mulge0	$⊢ ((L (F) \in ℝ \land 0 \leq L (F)) \land (M (G) \in ℝ \land 0 \leq M (G))) \to 0 \leq L (F) M (G)$
29	23 27 28	syl2an	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to 0 \leq L (F) M (G)$
30	10	ad2antrr	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to U \in NrmGrp$
31	12	ad2antrr	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to F \in (T GrpHom U)$
32		eqid	$⊢ {Base}_{T} = {Base}_{T}$
33		eqid	$⊢ {Base}_{U} = {Base}_{U}$
34	32 33	ghmf	$⊢ F \in (T GrpHom U) \to F : {Base}_{T} ⟶ {Base}_{U}$
35	31 34	syl	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to F : {Base}_{T} ⟶ {Base}_{U}$
36	13	ad2antlr	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to G \in (S GrpHom T)$
37	4 32	ghmf	$⊢ G \in (S GrpHom T) \to G : {Base}_{S} ⟶ {Base}_{T}$
38	36 37	syl	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to G : {Base}_{S} ⟶ {Base}_{T}$
39		simprl	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to x \in {Base}_{S}$
40	38 39	ffvelrnd	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to G (x) \in {Base}_{T}$
41	35 40	ffvelrnd	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to F (G (x)) \in {Base}_{U}$
42	33 6	nmcl	$⊢ (U \in NrmGrp \land F (G (x)) \in {Base}_{U}) \to norm (U) (F (G (x))) \in ℝ$
43	30 41 42	syl2anc	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (U) (F (G (x))) \in ℝ$
44	16	ad2antrr	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to L (F) \in ℝ$
45	20	ad2antrr	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to T \in NrmGrp$
46		eqid	$⊢ norm (T) = norm (T)$
47	32 46	nmcl	$⊢ (T \in NrmGrp \land G (x) \in {Base}_{T}) \to norm (T) (G (x)) \in ℝ$
48	45 40 47	syl2anc	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) (G (x)) \in ℝ$
49	44 48	remulcld	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to L (F) norm (T) (G (x)) \in ℝ$
50	17	ad2antlr	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to M (G) \in ℝ$
51	4 5	nmcl	$⊢ (S \in NrmGrp \land x \in {Base}_{S}) \to norm (S) (x) \in ℝ$
52	8 51	sylan	$⊢ (G \in (S NGHom T) \land x \in {Base}_{S}) \to norm (S) (x) \in ℝ$
53	52	ad2ant2lr	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (S) (x) \in ℝ$
54	50 53	remulcld	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to M (G) norm (S) (x) \in ℝ$
55	44 54	remulcld	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to L (F) M (G) norm (S) (x) \in ℝ$
56		simpll	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to F \in (T NGHom U)$
57	2 32 46 6	nmoi	$⊢ (F \in (T NGHom U) \land G (x) \in {Base}_{T}) \to norm (U) (F (G (x))) \leq L (F) norm (T) (G (x))$
58	56 40 57	syl2anc	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (U) (F (G (x))) \leq L (F) norm (T) (G (x))$
59	23	ad2antrr	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to (L (F) \in ℝ \land 0 \leq L (F))$
60	3 4 5 46	nmoi	$⊢ (G \in (S NGHom T) \land x \in {Base}_{S}) \to norm (T) (G (x)) \leq M (G) norm (S) (x)$
61	60	ad2ant2lr	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) (G (x)) \leq M (G) norm (S) (x)$
62		lemul2a	$⊢ ((norm (T) (G (x)) \in ℝ \land M (G) norm (S) (x) \in ℝ \land (L (F) \in ℝ \land 0 \leq L (F))) \land norm (T) (G (x)) \leq M (G) norm (S) (x)) \to L (F) norm (T) (G (x)) \leq L (F) M (G) norm (S) (x)$
63	48 54 59 61 62	syl31anc	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to L (F) norm (T) (G (x)) \leq L (F) M (G) norm (S) (x)$
64	43 49 55 58 63	letrd	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (U) (F (G (x))) \leq L (F) M (G) norm (S) (x)$
65		fvco3	$⊢ (G : {Base}_{S} ⟶ {Base}_{T} \land x \in {Base}_{S}) \to (F \circ G) (x) = F (G (x))$
66	38 39 65	syl2anc	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to (F \circ G) (x) = F (G (x))$
67	66	fveq2d	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (U) ((F \circ G) (x)) = norm (U) (F (G (x)))$
68	44	recnd	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to L (F) \in ℂ$
69	50	recnd	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to M (G) \in ℂ$
70	53	recnd	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (S) (x) \in ℂ$
71	68 69 70	mulassd	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to L (F) M (G) norm (S) (x) = L (F) M (G) norm (S) (x)$
72	64 67 71	3brtr4d	$⊢ ((F \in (T NGHom U) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (U) ((F \circ G) (x)) \leq L (F) M (G) norm (S) (x)$
73	1 4 5 6 7 9 11 15 19 29 72	nmolb2d	$⊢ (F \in (T NGHom U) \land G \in (S NGHom T)) \to N (F \circ G) \leq L (F) M (G)$

Metamath Proof Explorer

Theorem nmoco

Proof