This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nlmlmod

Description: A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion nlmlmod ( 𝑊 ∈ NrmMod → 𝑊 ∈ LMod )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
2 eqid ⊢ ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
3 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
4 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
6 eqid ⊢ ( norm ‘ ( Scalar ‘ 𝑊 ) ) = ( norm ‘ ( Scalar ‘ 𝑊 ) )
7 1 2 3 4 5 6 isnlm ⊢ ( 𝑊 ∈ NrmMod ↔ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) ∈ NrmRing ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( norm ‘ 𝑊 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑥 ) · ( ( norm ‘ 𝑊 ) ‘ 𝑦 ) ) ) )
8 7 simplbi ⊢ ( 𝑊 ∈ NrmMod → ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) ∈ NrmRing ) )
9 8 simp2d ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ LMod )