Metamath Proof Explorer

Theorem 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 
|- .+ = ( +g ` T )
Assertion nmotri 
|- ( ( T e. Abel /\ F e. ( S NGHom T ) /\ G e. ( S NGHom T ) ) -> ( N ` ( F oF .+ G ) ) <_ ( ( N ` F ) + ( N ` G ) ) )

Proof

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