Theorem idnmhm

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

	Ref	Expression
Hypothesis	0nmhm.1	⊢ 𝑉 = ( Base ‘ 𝑆 )
Assertion	idnmhm	⊢ ( 𝑆 ∈ NrmMod → ( I ↾ 𝑉 ) ∈ ( 𝑆 NMHom 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		0nmhm.1	⊢ 𝑉 = ( Base ‘ 𝑆 )
2		id	⊢ ( 𝑆 ∈ NrmMod → 𝑆 ∈ NrmMod )
3		nlmlmod	⊢ ( 𝑆 ∈ NrmMod → 𝑆 ∈ LMod )
4	1	idlmhm	⊢ ( 𝑆 ∈ LMod → ( I ↾ 𝑉 ) ∈ ( 𝑆 LMHom 𝑆 ) )
5	3 4	syl	⊢ ( 𝑆 ∈ NrmMod → ( I ↾ 𝑉 ) ∈ ( 𝑆 LMHom 𝑆 ) )
6		nlmngp	⊢ ( 𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp )
7	1	idnghm	⊢ ( 𝑆 ∈ NrmGrp → ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) )
8	6 7	syl	⊢ ( 𝑆 ∈ NrmMod → ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) )
9	5 8	jca	⊢ ( 𝑆 ∈ NrmMod → ( ( I ↾ 𝑉 ) ∈ ( 𝑆 LMHom 𝑆 ) ∧ ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) ) )
10		isnmhm	⊢ ( ( I ↾ 𝑉 ) ∈ ( 𝑆 NMHom 𝑆 ) ↔ ( ( 𝑆 ∈ NrmMod ∧ 𝑆 ∈ NrmMod ) ∧ ( ( I ↾ 𝑉 ) ∈ ( 𝑆 LMHom 𝑆 ) ∧ ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) ) ) )
11	2 2 9 10	syl21anbrc	⊢ ( 𝑆 ∈ NrmMod → ( I ↾ 𝑉 ) ∈ ( 𝑆 NMHom 𝑆 ) )