df-nmhm

Description: Define a normed module homomorphism, also known as a bounded linear operator. This is a module homomorphism (a linear function) such that the operator norm is finite, or equivalently there is a constant c such that... (Contributed by Mario Carneiro, 18-Oct-2015)

		Ref	Expression
	Assertion	df-nmhm	⊢ NMHom = ( 𝑠 ∈ NrmMod , 𝑡 ∈ NrmMod ↦ ( ( 𝑠 LMHom 𝑡 ) ∩ ( 𝑠 NGHom 𝑡 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnmhm	⊢ NMHom
1		vs	⊢ 𝑠
2		cnlm	⊢ NrmMod
3		vt	⊢ 𝑡
4	1	cv	⊢ 𝑠
5		clmhm	⊢ LMHom
6	3	cv	⊢ 𝑡
7	4 6 5	co	⊢ ( 𝑠 LMHom 𝑡 )
8		cnghm	⊢ NGHom
9	4 6 8	co	⊢ ( 𝑠 NGHom 𝑡 )
10	7 9	cin	⊢ ( ( 𝑠 LMHom 𝑡 ) ∩ ( 𝑠 NGHom 𝑡 ) )
11	1 3 2 2 10	cmpo	⊢ ( 𝑠 ∈ NrmMod , 𝑡 ∈ NrmMod ↦ ( ( 𝑠 LMHom 𝑡 ) ∩ ( 𝑠 NGHom 𝑡 ) ) )
12	0 11	wceq	⊢ NMHom = ( 𝑠 ∈ NrmMod , 𝑡 ∈ NrmMod ↦ ( ( 𝑠 LMHom 𝑡 ) ∩ ( 𝑠 NGHom 𝑡 ) ) )

Metamath Proof Explorer

Definition df-nmhm

Detailed syntax breakdown