Metamath Proof Explorer

Theorem 0nghm

Description: The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypotheses 0nghm.2 
|- V = ( Base ` S )
0nghm.3 
|- .0. = ( 0g ` T )
Assertion 0nghm 
|- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( V X. { .0. } ) e. ( S NGHom T ) )

Proof

Step Hyp Ref Expression
1 0nghm.2 
 |-  V = ( Base ` S )
2 0nghm.3 
 |-  .0. = ( 0g ` T )
3 eqid 
 |-  ( S normOp T ) = ( S normOp T )
4 3 1 2 nmo0 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( ( S normOp T ) ` ( V X. { .0. } ) ) = 0 )
5 0re 
 |-  0 e. RR
6 4 5 eqeltrdi 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( ( S normOp T ) ` ( V X. { .0. } ) ) e. RR )
7 ngpgrp 
 |-  ( S e. NrmGrp -> S e. Grp )
8 ngpgrp 
 |-  ( T e. NrmGrp -> T e. Grp )
9 2 1 0ghm 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( V X. { .0. } ) e. ( S GrpHom T ) )
10 7 8 9 syl2an 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( V X. { .0. } ) e. ( S GrpHom T ) )
11 3 isnghm2 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ ( V X. { .0. } ) e. ( S GrpHom T ) ) -> ( ( V X. { .0. } ) e. ( S NGHom T ) <-> ( ( S normOp T ) ` ( V X. { .0. } ) ) e. RR ) )
12 10 11 mpd3an3 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( ( V X. { .0. } ) e. ( S NGHom T ) <-> ( ( S normOp T ) ` ( V X. { .0. } ) ) e. RR ) )
13 6 12 mpbird 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( V X. { .0. } ) e. ( S NGHom T ) )