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

Metamath Proof Explorer

Theorem nlmnrg

Description: The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypothesis nlmnrg.1 ⊢ F = Scalar ⁡ W
Assertion nlmnrg ⊢ W ∈ NrmMod → F ∈ NrmRing

Proof

Step Hyp Ref Expression
1 nlmnrg.1 ⊢ F = Scalar ⁡ W
2 eqid ⊢ Base W = Base W
3 eqid ⊢ norm ⁡ W = norm ⁡ W
4 eqid ⊢ ⋅ W = ⋅ W
5 eqid ⊢ Base F = Base F
6 eqid ⊢ norm ⁡ F = norm ⁡ F
7 2 3 4 1 5 6 isnlm ⊢ W ∈ NrmMod ↔ W ∈ NrmGrp ∧ W ∈ LMod ∧ F ∈ NrmRing ∧ ∀ x ∈ Base F ∀ y ∈ Base W norm ⁡ W ⁡ x ⋅ W y = norm ⁡ F ⁡ x ⁢ norm ⁡ W ⁡ y
8 7 simplbi ⊢ W ∈ NrmMod → W ∈ NrmGrp ∧ W ∈ LMod ∧ F ∈ NrmRing
9 8 simp3d ⊢ W ∈ NrmMod → F ∈ NrmRing