Metamath Proof Explorer

Theorem nlmngp

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

Ref Expression
Assertion nlmngp ⊢ W ∈ NrmMod → W ∈ NrmGrp

Proof

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