nmotri

Description: Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015)

	Ref	Expression
Hypotheses	nmotri.1	$⊢ N = S normOp T$
	nmotri.p	$⊢ \underset{˙}{+} = +_{T}$
Assertion	nmotri	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to N (F {\underset{˙}{+}}_{f} G) \leq N (F) + N (G)$

Proof

Step	Hyp	Ref	Expression
1		nmotri.1	$⊢ N = S normOp T$
2		nmotri.p	$⊢ \underset{˙}{+} = +_{T}$
3		eqid	$⊢ {Base}_{S} = {Base}_{S}$
4		eqid	$⊢ norm (S) = norm (S)$
5		eqid	$⊢ norm (T) = norm (T)$
6		eqid	$⊢ 0_{S} = 0_{S}$
7		nghmrcl1	$⊢ F \in (S NGHom T) \to S \in NrmGrp$
8	7	3ad2ant2	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to S \in NrmGrp$
9		nghmrcl2	$⊢ F \in (S NGHom T) \to T \in NrmGrp$
10	9	3ad2ant2	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to T \in NrmGrp$
11		id	$⊢ T \in Abel \to T \in Abel$
12		nghmghm	$⊢ F \in (S NGHom T) \to F \in (S GrpHom T)$
13		nghmghm	$⊢ G \in (S NGHom T) \to G \in (S GrpHom T)$
14	2	ghmplusg	$⊢ (T \in Abel \land F \in (S GrpHom T) \land G \in (S GrpHom T)) \to F {\underset{˙}{+}}_{f} G \in (S GrpHom T)$
15	11 12 13 14	syl3an	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to F {\underset{˙}{+}}_{f} G \in (S GrpHom T)$
16	1	nghmcl	$⊢ F \in (S NGHom T) \to N (F) \in ℝ$
17	16	3ad2ant2	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to N (F) \in ℝ$
18	1	nghmcl	$⊢ G \in (S NGHom T) \to N (G) \in ℝ$
19	18	3ad2ant3	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to N (G) \in ℝ$
20	17 19	readdcld	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to N (F) + N (G) \in ℝ$
21	12	3ad2ant2	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to F \in (S GrpHom T)$
22	1	nmoge0	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to 0 \leq N (F)$
23	8 10 21 22	syl3anc	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to 0 \leq N (F)$
24	13	3ad2ant3	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to G \in (S GrpHom T)$
25	1	nmoge0	$⊢ (S \in NrmGrp \land T \in NrmGrp \land G \in (S GrpHom T)) \to 0 \leq N (G)$
26	8 10 24 25	syl3anc	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to 0 \leq N (G)$
27	17 19 23 26	addge0d	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to 0 \leq N (F) + N (G)$
28	10	adantr	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to T \in NrmGrp$
29		ngpgrp	$⊢ T \in NrmGrp \to T \in Grp$
30	28 29	syl	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to T \in Grp$
31	21	adantr	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to F \in (S GrpHom T)$
32		eqid	$⊢ {Base}_{T} = {Base}_{T}$
33	3 32	ghmf	$⊢ F \in (S GrpHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
34	31 33	syl	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to F : {Base}_{S} ⟶ {Base}_{T}$
35		simprl	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to x \in {Base}_{S}$
36	34 35	ffvelrnd	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to F (x) \in {Base}_{T}$
37	24	adantr	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to G \in (S GrpHom T)$
38	3 32	ghmf	$⊢ G \in (S GrpHom T) \to G : {Base}_{S} ⟶ {Base}_{T}$
39	37 38	syl	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to G : {Base}_{S} ⟶ {Base}_{T}$
40	39 35	ffvelrnd	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to G (x) \in {Base}_{T}$
41	32 2	grpcl	$⊢ (T \in Grp \land F (x) \in {Base}_{T} \land G (x) \in {Base}_{T}) \to F (x) \underset{˙}{+} G (x) \in {Base}_{T}$
42	30 36 40 41	syl3anc	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to F (x) \underset{˙}{+} G (x) \in {Base}_{T}$
43	32 5	nmcl	$⊢ (T \in NrmGrp \land F (x) \underset{˙}{+} G (x) \in {Base}_{T}) \to norm (T) (F (x) \underset{˙}{+} G (x)) \in ℝ$
44	28 42 43	syl2anc	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) (F (x) \underset{˙}{+} G (x)) \in ℝ$
45	32 5	nmcl	$⊢ (T \in NrmGrp \land F (x) \in {Base}_{T}) \to norm (T) (F (x)) \in ℝ$
46	28 36 45	syl2anc	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) (F (x)) \in ℝ$
47	32 5	nmcl	$⊢ (T \in NrmGrp \land G (x) \in {Base}_{T}) \to norm (T) (G (x)) \in ℝ$
48	28 40 47	syl2anc	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) (G (x)) \in ℝ$
49	46 48	readdcld	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) (F (x)) + norm (T) (G (x)) \in ℝ$
50	17	adantr	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to N (F) \in ℝ$
51		simpl	$⊢ (x \in {Base}_{S} \land x \neq 0_{S}) \to x \in {Base}_{S}$
52	3 4	nmcl	$⊢ (S \in NrmGrp \land x \in {Base}_{S}) \to norm (S) (x) \in ℝ$
53	8 51 52	syl2an	$⊢ ((T \in Abel \land F \in (S NGHom T) \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	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to N (F) norm (S) (x) \in ℝ$
55	19	adantr	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to N (G) \in ℝ$
56	55 53	remulcld	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to N (G) norm (S) (x) \in ℝ$
57	54 56	readdcld	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to N (F) norm (S) (x) + N (G) norm (S) (x) \in ℝ$
58	32 5 2	nmtri	$⊢ (T \in NrmGrp \land F (x) \in {Base}_{T} \land G (x) \in {Base}_{T}) \to norm (T) (F (x) \underset{˙}{+} G (x)) \leq norm (T) (F (x)) + norm (T) (G (x))$
59	28 36 40 58	syl3anc	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) (F (x) \underset{˙}{+} G (x)) \leq norm (T) (F (x)) + norm (T) (G (x))$
60		simpl2	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to F \in (S NGHom T)$
61	1 3 4 5	nmoi	$⊢ (F \in (S NGHom T) \land x \in {Base}_{S}) \to norm (T) (F (x)) \leq N (F) norm (S) (x)$
62	60 35 61	syl2anc	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) (F (x)) \leq N (F) norm (S) (x)$
63		simpl3	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to G \in (S NGHom T)$
64	1 3 4 5	nmoi	$⊢ (G \in (S NGHom T) \land x \in {Base}_{S}) \to norm (T) (G (x)) \leq N (G) norm (S) (x)$
65	63 35 64	syl2anc	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) (G (x)) \leq N (G) norm (S) (x)$
66	46 48 54 56 62 65	le2addd	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) (F (x)) + norm (T) (G (x)) \leq N (F) norm (S) (x) + N (G) norm (S) (x)$
67	44 49 57 59 66	letrd	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) (F (x) \underset{˙}{+} G (x)) \leq N (F) norm (S) (x) + N (G) norm (S) (x)$
68	34	ffnd	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to F Fn {Base}_{S}$
69	39	ffnd	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to G Fn {Base}_{S}$
70		fvexd	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to {Base}_{S} \in V$
71		fnfvof	$⊢ ((F Fn {Base}_{S} \land G Fn {Base}_{S}) \land ({Base}_{S} \in V \land x \in {Base}_{S})) \to (F {\underset{˙}{+}}_{f} G) (x) = F (x) \underset{˙}{+} G (x)$
72	68 69 70 35 71	syl22anc	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to (F {\underset{˙}{+}}_{f} G) (x) = F (x) \underset{˙}{+} G (x)$
73	72	fveq2d	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) ((F {\underset{˙}{+}}_{f} G) (x)) = norm (T) (F (x) \underset{˙}{+} G (x))$
74	50	recnd	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to N (F) \in ℂ$
75	55	recnd	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to N (G) \in ℂ$
76	53	recnd	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (S) (x) \in ℂ$
77	74 75 76	adddird	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to (N (F) + N (G)) norm (S) (x) = N (F) norm (S) (x) + N (G) norm (S) (x)$
78	67 73 77	3brtr4d	$⊢ ((T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \land (x \in {Base}_{S} \land x \neq 0_{S})) \to norm (T) ((F {\underset{˙}{+}}_{f} G) (x)) \leq (N (F) + N (G)) norm (S) (x)$
79	1 3 4 5 6 8 10 15 20 27 78	nmolb2d	$⊢ (T \in Abel \land F \in (S NGHom T) \land G \in (S NGHom T)) \to N (F {\underset{˙}{+}}_{f} G) \leq N (F) + N (G)$

Metamath Proof Explorer

Theorem nmotri

Proof