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 ⊢ 𝑉 = ( 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 𝑆 ) )