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

Metamath Proof Explorer

Theorem lmodgrp

Description: A left module is a group. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 25-Jun-2014)

Ref Expression
Assertion lmodgrp ⊢ W ∈ LMod → W ∈ Grp

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base W = Base W
2 eqid ⊢ + W = + W
3 eqid ⊢ ⋅ W = ⋅ W
4 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
5 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
6 eqid ⊢ + Scalar ⁡ W = + Scalar ⁡ W
7 eqid ⊢ ⋅ Scalar ⁡ W = ⋅ Scalar ⁡ W
8 eqid ⊢ 1 Scalar ⁡ W = 1 Scalar ⁡ W
9 1 2 3 4 5 6 7 8 islmod ⊢ W ∈ LMod ↔ W ∈ Grp ∧ Scalar ⁡ W ∈ Ring ∧ ∀ q ∈ Base Scalar ⁡ W ∀ r ∈ Base Scalar ⁡ W ∀ x ∈ Base W ∀ w ∈ Base W r ⋅ W w ∈ Base W ∧ r ⋅ W w + W x = r ⋅ W w + W r ⋅ W x ∧ q + Scalar ⁡ W r ⋅ W w = q ⋅ W w + W r ⋅ W w ∧ q ⋅ Scalar ⁡ W r ⋅ W w = q ⋅ W r ⋅ W w ∧ 1 Scalar ⁡ W ⋅ W w = w
10 9 simp1bi ⊢ W ∈ LMod → W ∈ Grp