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