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 \in NrmMod \to {I ↾}_{V} \in (S NMHom S)$

Step	Hyp	Ref	Expression
1		0nmhm.1	$⊢ V = {Base}_{S}$
2		id	$⊢ S \in NrmMod \to S \in NrmMod$
3		nlmlmod	$⊢ S \in NrmMod \to S \in LMod$
4	1	idlmhm	$⊢ S \in LMod \to {I ↾}_{V} \in (S LMHom S)$
5	3 4	syl	$⊢ S \in NrmMod \to {I ↾}_{V} \in (S LMHom S)$
6		nlmngp	$⊢ S \in NrmMod \to S \in NrmGrp$
7	1	idnghm	$⊢ S \in NrmGrp \to {I ↾}_{V} \in (S NGHom S)$
8	6 7	syl	$⊢ S \in NrmMod \to {I ↾}_{V} \in (S NGHom S)$
9	5 8	jca	$⊢ S \in NrmMod \to ({I ↾}_{V} \in (S LMHom S) \land {I ↾}_{V} \in (S NGHom S))$
10		isnmhm	$⊢ {I ↾}_{V} \in (S NMHom S) \leftrightarrow ((S \in NrmMod \land S \in NrmMod) \land ({I ↾}_{V} \in (S LMHom S) \land {I ↾}_{V} \in (S NGHom S)))$
11	2 2 9 10	syl21anbrc	$⊢ S \in NrmMod \to {I ↾}_{V} \in (S NMHom S)$

Metamath Proof Explorer