| Step |
Hyp |
Ref |
Expression |
| 1 |
|
nmofval.1 |
|- N = ( S normOp T ) |
| 2 |
1
|
nghmfval |
|- ( S NGHom T ) = ( `' N " RR ) |
| 3 |
2
|
eleq2i |
|- ( F e. ( S NGHom T ) <-> F e. ( `' N " RR ) ) |
| 4 |
|
n0i |
|- ( F e. ( `' N " RR ) -> -. ( `' N " RR ) = (/) ) |
| 5 |
|
nmoffn |
|- normOp Fn ( NrmGrp X. NrmGrp ) |
| 6 |
5
|
fndmi |
|- dom normOp = ( NrmGrp X. NrmGrp ) |
| 7 |
6
|
ndmov |
|- ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> ( S normOp T ) = (/) ) |
| 8 |
1 7
|
eqtrid |
|- ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> N = (/) ) |
| 9 |
8
|
cnveqd |
|- ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> `' N = `' (/) ) |
| 10 |
|
cnv0 |
|- `' (/) = (/) |
| 11 |
9 10
|
eqtrdi |
|- ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> `' N = (/) ) |
| 12 |
11
|
imaeq1d |
|- ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> ( `' N " RR ) = ( (/) " RR ) ) |
| 13 |
|
0ima |
|- ( (/) " RR ) = (/) |
| 14 |
12 13
|
eqtrdi |
|- ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> ( `' N " RR ) = (/) ) |
| 15 |
4 14
|
nsyl2 |
|- ( F e. ( `' N " RR ) -> ( S e. NrmGrp /\ T e. NrmGrp ) ) |
| 16 |
1
|
nmof |
|- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N : ( S GrpHom T ) --> RR* ) |
| 17 |
|
ffn |
|- ( N : ( S GrpHom T ) --> RR* -> N Fn ( S GrpHom T ) ) |
| 18 |
|
elpreima |
|- ( N Fn ( S GrpHom T ) -> ( F e. ( `' N " RR ) <-> ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) ) |
| 19 |
16 17 18
|
3syl |
|- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( F e. ( `' N " RR ) <-> ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) ) |
| 20 |
15 19
|
biadanii |
|- ( F e. ( `' N " RR ) <-> ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) ) |
| 21 |
3 20
|
bitri |
|- ( F e. ( S NGHom T ) <-> ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) ) |