Theorem nmotri

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

	Ref	Expression
Hypotheses	nmotri.1	⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
	nmotri.p	⊢ + = ( +g ‘ 𝑇 )
Assertion	nmotri	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝑁 ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) + ( 𝑁 ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmotri.1	⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2		nmotri.p	⊢ + = ( +g ‘ 𝑇 )
3		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
4		eqid	⊢ ( norm ‘ 𝑆 ) = ( norm ‘ 𝑆 )
5		eqid	⊢ ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 )
6		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
7		nghmrcl1	⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑆 ∈ NrmGrp )
8	7	3ad2ant2	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝑆 ∈ NrmGrp )
9		nghmrcl2	⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑇 ∈ NrmGrp )
10	9	3ad2ant2	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝑇 ∈ NrmGrp )
11		id	⊢ ( 𝑇 ∈ Abel → 𝑇 ∈ Abel )
12		nghmghm	⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
13		nghmghm	⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) )
14	2	ghmplusg	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 GrpHom 𝑇 ) )
15	11 12 13 14	syl3an	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 GrpHom 𝑇 ) )
16	1	nghmcl	⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )
17	16	3ad2ant2	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )
18	1	nghmcl	⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → ( 𝑁 ‘ 𝐺 ) ∈ ℝ )
19	18	3ad2ant3	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝑁 ‘ 𝐺 ) ∈ ℝ )
20	17 19	readdcld	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( 𝑁 ‘ 𝐹 ) + ( 𝑁 ‘ 𝐺 ) ) ∈ ℝ )
21	12	3ad2ant2	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
22	1	nmoge0	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑁 ‘ 𝐹 ) )
23	8 10 21 22	syl3anc	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 0 ≤ ( 𝑁 ‘ 𝐹 ) )
24	13	3ad2ant3	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) )
25	1	nmoge0	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑁 ‘ 𝐺 ) )
26	8 10 24 25	syl3anc	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 0 ≤ ( 𝑁 ‘ 𝐺 ) )
27	17 19 23 26	addge0d	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 0 ≤ ( ( 𝑁 ‘ 𝐹 ) + ( 𝑁 ‘ 𝐺 ) ) )
28	10	adantr	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑇 ∈ NrmGrp )
29		ngpgrp	⊢ ( 𝑇 ∈ NrmGrp → 𝑇 ∈ Grp )
30	28 29	syl	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑇 ∈ Grp )
31	21	adantr	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
32		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
33	3 32	ghmf	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
34	31 33	syl	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
35		simprl	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
36	34 35	ffvelcdmd	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
37	24	adantr	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) )
38	3 32	ghmf	⊢ ( 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
39	37 38	syl	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
40	39 35	ffvelcdmd	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
41	32 2	grpcl	⊢ ( ( 𝑇 ∈ Grp ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) )
42	30 36 40 41	syl3anc	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) )
43	32 5	nmcl	⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ )
44	28 42 43	syl2anc	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ )
45	32 5	nmcl	⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
46	28 36 45	syl2anc	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
47	32 5	nmcl	⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
48	28 40 47	syl2anc	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
49	46 48	readdcld	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) + ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ )
50	17	adantr	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ )
51		simpl	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
52	3 4	nmcl	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ )
53	8 51 52	syl2an	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℝ )
54	50 53	remulcld	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ∈ ℝ )
55	19	adantr	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑁 ‘ 𝐺 ) ∈ ℝ )
56	55 53	remulcld	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑁 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ∈ ℝ )
57	54 56	readdcld	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) + ( ( 𝑁 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ) ∈ ℝ )
58	32 5 2	nmtri	⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) + ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
59	28 36 40 58	syl3anc	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) + ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
60		simpl2	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) )
61	1 3 4 5	nmoi	⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
62	60 35 61	syl2anc	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
63		simpl3	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) )
64	1 3 4 5	nmoi	⊢ ( ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
65	63 35 64	syl2anc	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ ( ( 𝑁 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
66	46 48 54 56 62 65	le2addd	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) + ( ( norm ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) + ( ( 𝑁 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ) )
67	44 49 57 59 66	letrd	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) + ( ( 𝑁 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ) )
68	34	ffnd	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
69	39	ffnd	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → 𝐺 Fn ( Base ‘ 𝑆 ) )
70		fvexd	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( Base ‘ 𝑆 ) ∈ V )
71		fnfvof	⊢ ( ( ( 𝐹 Fn ( Base ‘ 𝑆 ) ∧ 𝐺 Fn ( Base ‘ 𝑆 ) ) ∧ ( ( Base ‘ 𝑆 ) ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
72	68 69 70 35 71	syl22anc	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) )
73	72	fveq2d	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ) = ( ( norm ‘ 𝑇 ) ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) )
74	50	recnd	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℂ )
75	55	recnd	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( 𝑁 ‘ 𝐺 ) ∈ ℂ )
76	53	recnd	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ∈ ℂ )
77	74 75 76	adddird	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( ( 𝑁 ‘ 𝐹 ) + ( 𝑁 ‘ 𝐺 ) ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) = ( ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) + ( ( 𝑁 ‘ 𝐺 ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) ) )
78	67 73 77	3brtr4d	⊢ ( ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑆 ) ) ) → ( ( norm ‘ 𝑇 ) ‘ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑥 ) ) ≤ ( ( ( 𝑁 ‘ 𝐹 ) + ( 𝑁 ‘ 𝐺 ) ) · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) )
79	1 3 4 5 6 8 10 15 20 27 78	nmolb2d	⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝑁 ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) + ( 𝑁 ‘ 𝐺 ) ) )