Metamath Proof Explorer

Theorem idnghm

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

Ref Expression
Hypothesis idnghm.2 
|- V = ( Base ` S )
Assertion idnghm 
|- ( S e. NrmGrp -> ( _I |` V ) e. ( S NGHom S ) )

Proof

Step Hyp Ref Expression
1 idnghm.2 
 |-  V = ( Base ` S )
2 eqid 
 |-  ( S normOp S ) = ( S normOp S )
3 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
4 2 1 3 nmoid 
 |-  ( ( S e. NrmGrp /\ { ( 0g ` S ) } C. V ) -> ( ( S normOp S ) ` ( _I |` V ) ) = 1 )
5 1re 
 |-  1 e. RR
6 4 5 eqeltrdi 
 |-  ( ( S e. NrmGrp /\ { ( 0g ` S ) } C. V ) -> ( ( S normOp S ) ` ( _I |` V ) ) e. RR )
7 eleq2 
 |-  ( { ( 0g ` S ) } = V -> ( x e. { ( 0g ` S ) } <-> x e. V ) )
8 7 biimpar 
 |-  ( ( { ( 0g ` S ) } = V /\ x e. V ) -> x e. { ( 0g ` S ) } )
9 elsni 
 |-  ( x e. { ( 0g ` S ) } -> x = ( 0g ` S ) )
10 8 9 syl 
 |-  ( ( { ( 0g ` S ) } = V /\ x e. V ) -> x = ( 0g ` S ) )
11 10 mpteq2dva 
 |-  ( { ( 0g ` S ) } = V -> ( x e. V |-> x ) = ( x e. V |-> ( 0g ` S ) ) )
12 mptresid 
 |-  ( _I |` V ) = ( x e. V |-> x )
13 fconstmpt 
 |-  ( V X. { ( 0g ` S ) } ) = ( x e. V |-> ( 0g ` S ) )
14 11 12 13 3eqtr4g 
 |-  ( { ( 0g ` S ) } = V -> ( _I |` V ) = ( V X. { ( 0g ` S ) } ) )
15 14 fveq2d 
 |-  ( { ( 0g ` S ) } = V -> ( ( S normOp S ) ` ( _I |` V ) ) = ( ( S normOp S ) ` ( V X. { ( 0g ` S ) } ) ) )
16 2 1 3 nmo0 
 |-  ( ( S e. NrmGrp /\ S e. NrmGrp ) -> ( ( S normOp S ) ` ( V X. { ( 0g ` S ) } ) ) = 0 )
17 16 anidms 
 |-  ( S e. NrmGrp -> ( ( S normOp S ) ` ( V X. { ( 0g ` S ) } ) ) = 0 )
18 15 17 sylan9eqr 
 |-  ( ( S e. NrmGrp /\ { ( 0g ` S ) } = V ) -> ( ( S normOp S ) ` ( _I |` V ) ) = 0 )
19 0re 
 |-  0 e. RR
20 18 19 eqeltrdi 
 |-  ( ( S e. NrmGrp /\ { ( 0g ` S ) } = V ) -> ( ( S normOp S ) ` ( _I |` V ) ) e. RR )
21 ngpgrp 
 |-  ( S e. NrmGrp -> S e. Grp )
22 1 3 grpidcl 
 |-  ( S e. Grp -> ( 0g ` S ) e. V )
23 21 22 syl 
 |-  ( S e. NrmGrp -> ( 0g ` S ) e. V )
24 23 snssd 
 |-  ( S e. NrmGrp -> { ( 0g ` S ) } C_ V )
25 sspss 
 |-  ( { ( 0g ` S ) } C_ V <-> ( { ( 0g ` S ) } C. V \/ { ( 0g ` S ) } = V ) )
26 24 25 sylib 
 |-  ( S e. NrmGrp -> ( { ( 0g ` S ) } C. V \/ { ( 0g ` S ) } = V ) )
27 6 20 26 mpjaodan 
 |-  ( S e. NrmGrp -> ( ( S normOp S ) ` ( _I |` V ) ) e. RR )
28 id 
 |-  ( S e. NrmGrp -> S e. NrmGrp )
29 1 idghm 
 |-  ( S e. Grp -> ( _I |` V ) e. ( S GrpHom S ) )
30 21 29 syl 
 |-  ( S e. NrmGrp -> ( _I |` V ) e. ( S GrpHom S ) )
31 2 isnghm2 
 |-  ( ( S e. NrmGrp /\ S e. NrmGrp /\ ( _I |` V ) e. ( S GrpHom S ) ) -> ( ( _I |` V ) e. ( S NGHom S ) <-> ( ( S normOp S ) ` ( _I |` V ) ) e. RR ) )
32 28 30 31 mpd3an23 
 |-  ( S e. NrmGrp -> ( ( _I |` V ) e. ( S NGHom S ) <-> ( ( S normOp S ) ` ( _I |` V ) ) e. RR ) )
33 27 32 mpbird 
 |-  ( S e. NrmGrp -> ( _I |` V ) e. ( S NGHom S ) )