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 e. ( S NMHom T ) -> F e. ( S LMHom T ) )

Step	Hyp	Ref	Expression
1		isnmhm	\|- ( F e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )
2	1	simprbi	\|- ( F e. ( S NMHom T ) -> ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) )
3	2	simpld	\|- ( F e. ( S NMHom T ) -> F e. ( S LMHom T ) )

Step

Hyp

Ref

Expression

 |-  ( F e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )

 |-  ( F e. ( S NMHom T ) -> ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) )

 |-  ( F e. ( S NMHom T ) -> F e. ( S LMHom T ) )