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