Metamath Proof Explorer

Theorem nmods

Description: Upper bound for the distance between the values of a bounded linear operator. (Contributed by Mario Carneiro, 22-Oct-2015)

Ref Expression
Hypotheses nmods.n 
|- N = ( S normOp T )
nmods.v 
|- V = ( Base ` S )
nmods.c 
|- C = ( dist ` S )
nmods.d 
|- D = ( dist ` T )
Assertion nmods 
|- ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( ( F ` A ) D ( F ` B ) ) <_ ( ( N ` F ) x. ( A C B ) ) )

Proof

Step Hyp Ref Expression
1 nmods.n 
 |-  N = ( S normOp T )
2 nmods.v 
 |-  V = ( Base ` S )
3 nmods.c 
 |-  C = ( dist ` S )
4 nmods.d 
 |-  D = ( dist ` T )
5 simp1 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> F e. ( S NGHom T ) )
6 nghmrcl1 
 |-  ( F e. ( S NGHom T ) -> S e. NrmGrp )
7 ngpgrp 
 |-  ( S e. NrmGrp -> S e. Grp )
8 6 7 syl 
 |-  ( F e. ( S NGHom T ) -> S e. Grp )
9 eqid 
 |-  ( -g ` S ) = ( -g ` S )
10 2 9 grpsubcl 
 |-  ( ( S e. Grp /\ A e. V /\ B e. V ) -> ( A ( -g ` S ) B ) e. V )
11 8 10 syl3an1 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( A ( -g ` S ) B ) e. V )
12 eqid 
 |-  ( norm ` S ) = ( norm ` S )
13 eqid 
 |-  ( norm ` T ) = ( norm ` T )
14 1 2 12 13 nmoi 
 |-  ( ( F e. ( S NGHom T ) /\ ( A ( -g ` S ) B ) e. V ) -> ( ( norm ` T ) ` ( F ` ( A ( -g ` S ) B ) ) ) <_ ( ( N ` F ) x. ( ( norm ` S ) ` ( A ( -g ` S ) B ) ) ) )
15 5 11 14 syl2anc 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( ( norm ` T ) ` ( F ` ( A ( -g ` S ) B ) ) ) <_ ( ( N ` F ) x. ( ( norm ` S ) ` ( A ( -g ` S ) B ) ) ) )
16 nghmrcl2 
 |-  ( F e. ( S NGHom T ) -> T e. NrmGrp )
17 16 3ad2ant1 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> T e. NrmGrp )
18 nghmghm 
 |-  ( F e. ( S NGHom T ) -> F e. ( S GrpHom T ) )
19 18 3ad2ant1 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> F e. ( S GrpHom T ) )
20 eqid 
 |-  ( Base ` T ) = ( Base ` T )
21 2 20 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : V --> ( Base ` T ) )
22 19 21 syl 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> F : V --> ( Base ` T ) )
23 simp2 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> A e. V )
24 22 23 ffvelrnd 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( F ` A ) e. ( Base ` T ) )
25 simp3 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> B e. V )
26 22 25 ffvelrnd 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( F ` B ) e. ( Base ` T ) )
27 eqid 
 |-  ( -g ` T ) = ( -g ` T )
28 13 20 27 4 ngpds 
 |-  ( ( T e. NrmGrp /\ ( F ` A ) e. ( Base ` T ) /\ ( F ` B ) e. ( Base ` T ) ) -> ( ( F ` A ) D ( F ` B ) ) = ( ( norm ` T ) ` ( ( F ` A ) ( -g ` T ) ( F ` B ) ) ) )
29 17 24 26 28 syl3anc 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( ( F ` A ) D ( F ` B ) ) = ( ( norm ` T ) ` ( ( F ` A ) ( -g ` T ) ( F ` B ) ) ) )
30 2 9 27 ghmsub 
 |-  ( ( F e. ( S GrpHom T ) /\ A e. V /\ B e. V ) -> ( F ` ( A ( -g ` S ) B ) ) = ( ( F ` A ) ( -g ` T ) ( F ` B ) ) )
31 18 30 syl3an1 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( F ` ( A ( -g ` S ) B ) ) = ( ( F ` A ) ( -g ` T ) ( F ` B ) ) )
32 31 fveq2d 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( ( norm ` T ) ` ( F ` ( A ( -g ` S ) B ) ) ) = ( ( norm ` T ) ` ( ( F ` A ) ( -g ` T ) ( F ` B ) ) ) )
33 29 32 eqtr4d 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( ( F ` A ) D ( F ` B ) ) = ( ( norm ` T ) ` ( F ` ( A ( -g ` S ) B ) ) ) )
34 12 2 9 3 ngpds 
 |-  ( ( S e. NrmGrp /\ A e. V /\ B e. V ) -> ( A C B ) = ( ( norm ` S ) ` ( A ( -g ` S ) B ) ) )
35 6 34 syl3an1 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( A C B ) = ( ( norm ` S ) ` ( A ( -g ` S ) B ) ) )
36 35 oveq2d 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( ( N ` F ) x. ( A C B ) ) = ( ( N ` F ) x. ( ( norm ` S ) ` ( A ( -g ` S ) B ) ) ) )
37 15 33 36 3brtr4d 
 |-  ( ( F e. ( S NGHom T ) /\ A e. V /\ B e. V ) -> ( ( F ` A ) D ( F ` B ) ) <_ ( ( N ` F ) x. ( A C B ) ) )