This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idnmhm

Description: The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypothesis 0nmhm.1 
|- V = ( Base ` S )
Assertion idnmhm 
|- ( S e. NrmMod -> ( _I |` V ) e. ( S NMHom S ) )

Proof

Step Hyp Ref Expression
1 0nmhm.1 
 |-  V = ( Base ` S )
2 id 
 |-  ( S e. NrmMod -> S e. NrmMod )
3 nlmlmod 
 |-  ( S e. NrmMod -> S e. LMod )
4 1 idlmhm 
 |-  ( S e. LMod -> ( _I |` V ) e. ( S LMHom S ) )
5 3 4 syl 
 |-  ( S e. NrmMod -> ( _I |` V ) e. ( S LMHom S ) )
6 nlmngp 
 |-  ( S e. NrmMod -> S e. NrmGrp )
7 1 idnghm 
 |-  ( S e. NrmGrp -> ( _I |` V ) e. ( S NGHom S ) )
8 6 7 syl 
 |-  ( S e. NrmMod -> ( _I |` V ) e. ( S NGHom S ) )
9 5 8 jca 
 |-  ( S e. NrmMod -> ( ( _I |` V ) e. ( S LMHom S ) /\ ( _I |` V ) e. ( S NGHom S ) ) )
10 isnmhm 
 |-  ( ( _I |` V ) e. ( S NMHom S ) <-> ( ( S e. NrmMod /\ S e. NrmMod ) /\ ( ( _I |` V ) e. ( S LMHom S ) /\ ( _I |` V ) e. ( S NGHom S ) ) ) )
11 2 2 9 10 syl21anbrc 
 |-  ( S e. NrmMod -> ( _I |` V ) e. ( S NMHom S ) )