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