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

Metamath Proof Explorer

Theorem lsslmod

Description: A submodule is a module. (Contributed by Stefan O'Rear, 12-Dec-2014)

Ref Expression
Hypotheses lsslss.x ⊢ X = W ↾ 𝑠 U
lsslss.s ⊢ S = LSubSp ⁡ W
Assertion lsslmod ⊢ W ∈ LMod ∧ U ∈ S → X ∈ LMod

Proof

Step Hyp Ref Expression
1 lsslss.x ⊢ X = W ↾ 𝑠 U
2 lsslss.s ⊢ S = LSubSp ⁡ W
3 eqid ⊢ Base W = Base W
4 1 3 2 islss3 ⊢ W ∈ LMod → U ∈ S ↔ U ⊆ Base W ∧ X ∈ LMod
5 4 simplbda ⊢ W ∈ LMod ∧ U ∈ S → X ∈ LMod