Metamath Proof Explorer

Theorem nghmfval

Description: A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypothesis nmofval.1 
|- N = ( S normOp T )
Assertion nghmfval 
|- ( S NGHom T ) = ( `' N " RR )

Proof

Step Hyp Ref Expression
1 nmofval.1 
 |-  N = ( S normOp T )
2 oveq12 
 |-  ( ( s = S /\ t = T ) -> ( s normOp t ) = ( S normOp T ) )
3 2 1 eqtr4di 
 |-  ( ( s = S /\ t = T ) -> ( s normOp t ) = N )
4 3 cnveqd 
 |-  ( ( s = S /\ t = T ) -> `' ( s normOp t ) = `' N )
5 4 imaeq1d 
 |-  ( ( s = S /\ t = T ) -> ( `' ( s normOp t ) " RR ) = ( `' N " RR ) )
6 df-nghm 
 |-  NGHom = ( s e. NrmGrp , t e. NrmGrp |-> ( `' ( s normOp t ) " RR ) )
7 1 ovexi 
 |-  N e. _V
8 7 cnvex 
 |-  `' N e. _V
9 8 imaex 
 |-  ( `' N " RR ) e. _V
10 5 6 9 ovmpoa 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( S NGHom T ) = ( `' N " RR ) )
11 6 mpondm0 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> ( S NGHom T ) = (/) )
12 nmoffn 
 |-  normOp Fn ( NrmGrp X. NrmGrp )
13 12 fndmi 
 |-  dom normOp = ( NrmGrp X. NrmGrp )
14 13 ndmov 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> ( S normOp T ) = (/) )
15 1 14 syl5eq 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> N = (/) )
16 15 cnveqd 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> `' N = `' (/) )
17 cnv0 
 |-  `' (/) = (/)
18 16 17 eqtrdi 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> `' N = (/) )
19 18 imaeq1d 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> ( `' N " RR ) = ( (/) " RR ) )
20 0ima 
 |-  ( (/) " RR ) = (/)
21 19 20 eqtrdi 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> ( `' N " RR ) = (/) )
22 11 21 eqtr4d 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> ( S NGHom T ) = ( `' N " RR ) )
23 10 22 pm2.61i 
 |-  ( S NGHom T ) = ( `' N " RR )