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. } ) ) )