Metamath Proof Explorer

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 ffvelrnd ⊢ ( ( ( 𝑇 ∈ 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 ffvelrnd ⊢ ( ( ( 𝑇 ∈ 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 + 𝐺 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) + ( 𝑁 ‘ 𝐺 ) ) )