Metamath Proof Explorer

Theorem nmhmlmhm

Description: A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Assertion nmhmlmhm ⊢ F ∈ S NMHom T → F ∈ S LMHom T

Proof

Step Hyp Ref Expression
1 isnmhm ⊢ F ∈ S NMHom T ↔ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F ∈ S LMHom T ∧ F ∈ S NGHom T
2 1 simprbi ⊢ F ∈ S NMHom T → F ∈ S LMHom T ∧ F ∈ S NGHom T
3 2 simpld ⊢ F ∈ S NMHom T → F ∈ S LMHom T