Metamath Proof Explorer


Theorem nmoeq0

Description: The operator norm is zero only for the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypotheses nmo0.1
|- N = ( S normOp T )
nmo0.2
|- V = ( Base ` S )
nmo0.3
|- .0. = ( 0g ` T )
Assertion nmoeq0
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( N ` F ) = 0 <-> F = ( V X. { .0. } ) ) )

Proof

Step Hyp Ref Expression
1 nmo0.1
 |-  N = ( S normOp T )
2 nmo0.2
 |-  V = ( Base ` S )
3 nmo0.3
 |-  .0. = ( 0g ` T )
4 id
 |-  ( ( N ` F ) = 0 -> ( N ` F ) = 0 )
5 0re
 |-  0 e. RR
6 4 5 eqeltrdi
 |-  ( ( N ` F ) = 0 -> ( N ` F ) e. RR )
7 1 isnghm2
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) e. RR ) )
8 7 biimpar
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) e. RR ) -> F e. ( S NGHom T ) )
9 6 8 sylan2
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) -> F e. ( S NGHom T ) )
10 eqid
 |-  ( norm ` S ) = ( norm ` S )
11 eqid
 |-  ( norm ` T ) = ( norm ` T )
12 1 2 10 11 nmoi
 |-  ( ( F e. ( S NGHom T ) /\ x e. V ) -> ( ( norm ` T ) ` ( F ` x ) ) <_ ( ( N ` F ) x. ( ( norm ` S ) ` x ) ) )
13 9 12 sylan
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( ( norm ` T ) ` ( F ` x ) ) <_ ( ( N ` F ) x. ( ( norm ` S ) ` x ) ) )
14 simplr
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( N ` F ) = 0 )
15 14 oveq1d
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( ( N ` F ) x. ( ( norm ` S ) ` x ) ) = ( 0 x. ( ( norm ` S ) ` x ) ) )
16 simpl1
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) -> S e. NrmGrp )
17 2 10 nmcl
 |-  ( ( S e. NrmGrp /\ x e. V ) -> ( ( norm ` S ) ` x ) e. RR )
18 16 17 sylan
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( ( norm ` S ) ` x ) e. RR )
19 18 recnd
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( ( norm ` S ) ` x ) e. CC )
20 19 mul02d
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( 0 x. ( ( norm ` S ) ` x ) ) = 0 )
21 15 20 eqtrd
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( ( N ` F ) x. ( ( norm ` S ) ` x ) ) = 0 )
22 13 21 breqtrd
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( ( norm ` T ) ` ( F ` x ) ) <_ 0 )
23 simpll2
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> T e. NrmGrp )
24 simpl3
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) -> F e. ( S GrpHom T ) )
25 eqid
 |-  ( Base ` T ) = ( Base ` T )
26 2 25 ghmf
 |-  ( F e. ( S GrpHom T ) -> F : V --> ( Base ` T ) )
27 24 26 syl
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) -> F : V --> ( Base ` T ) )
28 27 ffvelrnda
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( F ` x ) e. ( Base ` T ) )
29 25 11 nmge0
 |-  ( ( T e. NrmGrp /\ ( F ` x ) e. ( Base ` T ) ) -> 0 <_ ( ( norm ` T ) ` ( F ` x ) ) )
30 23 28 29 syl2anc
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> 0 <_ ( ( norm ` T ) ` ( F ` x ) ) )
31 25 11 nmcl
 |-  ( ( T e. NrmGrp /\ ( F ` x ) e. ( Base ` T ) ) -> ( ( norm ` T ) ` ( F ` x ) ) e. RR )
32 23 28 31 syl2anc
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( ( norm ` T ) ` ( F ` x ) ) e. RR )
33 letri3
 |-  ( ( ( ( norm ` T ) ` ( F ` x ) ) e. RR /\ 0 e. RR ) -> ( ( ( norm ` T ) ` ( F ` x ) ) = 0 <-> ( ( ( norm ` T ) ` ( F ` x ) ) <_ 0 /\ 0 <_ ( ( norm ` T ) ` ( F ` x ) ) ) ) )
34 32 5 33 sylancl
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( ( ( norm ` T ) ` ( F ` x ) ) = 0 <-> ( ( ( norm ` T ) ` ( F ` x ) ) <_ 0 /\ 0 <_ ( ( norm ` T ) ` ( F ` x ) ) ) ) )
35 22 30 34 mpbir2and
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( ( norm ` T ) ` ( F ` x ) ) = 0 )
36 25 11 3 nmeq0
 |-  ( ( T e. NrmGrp /\ ( F ` x ) e. ( Base ` T ) ) -> ( ( ( norm ` T ) ` ( F ` x ) ) = 0 <-> ( F ` x ) = .0. ) )
37 23 28 36 syl2anc
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( ( ( norm ` T ) ` ( F ` x ) ) = 0 <-> ( F ` x ) = .0. ) )
38 35 37 mpbid
 |-  ( ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) /\ x e. V ) -> ( F ` x ) = .0. )
39 38 mpteq2dva
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) -> ( x e. V |-> ( F ` x ) ) = ( x e. V |-> .0. ) )
40 27 feqmptd
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) -> F = ( x e. V |-> ( F ` x ) ) )
41 fconstmpt
 |-  ( V X. { .0. } ) = ( x e. V |-> .0. )
42 41 a1i
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) -> ( V X. { .0. } ) = ( x e. V |-> .0. ) )
43 39 40 42 3eqtr4d
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( N ` F ) = 0 ) -> F = ( V X. { .0. } ) )
44 43 ex
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( N ` F ) = 0 -> F = ( V X. { .0. } ) ) )
45 1 2 3 nmo0
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( N ` ( V X. { .0. } ) ) = 0 )
46 45 3adant3
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` ( V X. { .0. } ) ) = 0 )
47 fveqeq2
 |-  ( F = ( V X. { .0. } ) -> ( ( N ` F ) = 0 <-> ( N ` ( V X. { .0. } ) ) = 0 ) )
48 46 47 syl5ibrcom
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( F = ( V X. { .0. } ) -> ( N ` F ) = 0 ) )
49 44 48 impbid
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( N ` F ) = 0 <-> F = ( V X. { .0. } ) ) )