**Description:** All subspaces are subgroups. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref | Expression | ||
---|---|---|---|

Hypothesis | lsssubg.s | ⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) | |

Assertion | lsssssubg | ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | lsssubg.s | ⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) | |

2 | 1 | lsssubg | ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( SubGrp ‘ 𝑊 ) ) |

3 | 2 | ex | ⊢ ( 𝑊 ∈ LMod → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ( SubGrp ‘ 𝑊 ) ) ) |

4 | 3 | ssrdv | ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) ) |