# Metamath Proof Explorer

## Theorem lsssubg

Description: All subspaces are subgroups. (Contributed by Stefan O'Rear, 11-Dec-2014)

Ref Expression
Hypothesis lsssubg.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
Assertion lsssubg ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {U}\in \mathrm{SubGrp}\left({W}\right)$

### Proof

Step Hyp Ref Expression
1 lsssubg.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
2 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
3 2 1 lssss ${⊢}{U}\in {S}\to {U}\subseteq {\mathrm{Base}}_{{W}}$
4 3 adantl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {U}\subseteq {\mathrm{Base}}_{{W}}$
5 1 lssn0 ${⊢}{U}\in {S}\to {U}\ne \varnothing$
6 5 adantl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {U}\ne \varnothing$
7 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
8 7 1 lssvacl ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge \left({x}\in {U}\wedge {y}\in {U}\right)\right)\to {x}{+}_{{W}}{y}\in {U}$
9 8 anassrs ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge {x}\in {U}\right)\wedge {y}\in {U}\right)\to {x}{+}_{{W}}{y}\in {U}$
10 9 ralrimiva ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge {x}\in {U}\right)\to \forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{x}{+}_{{W}}{y}\in {U}$
11 eqid ${⊢}{inv}_{g}\left({W}\right)={inv}_{g}\left({W}\right)$
12 1 11 lssvnegcl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\wedge {x}\in {U}\right)\to {inv}_{g}\left({W}\right)\left({x}\right)\in {U}$
13 12 3expa ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge {x}\in {U}\right)\to {inv}_{g}\left({W}\right)\left({x}\right)\in {U}$
14 10 13 jca ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\wedge {x}\in {U}\right)\to \left(\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{x}{+}_{{W}}{y}\in {U}\wedge {inv}_{g}\left({W}\right)\left({x}\right)\in {U}\right)$
15 14 ralrimiva ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{x}{+}_{{W}}{y}\in {U}\wedge {inv}_{g}\left({W}\right)\left({x}\right)\in {U}\right)$
16 lmodgrp ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Grp}$
17 16 adantr ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {W}\in \mathrm{Grp}$
18 2 7 11 issubg2 ${⊢}{W}\in \mathrm{Grp}\to \left({U}\in \mathrm{SubGrp}\left({W}\right)↔\left({U}\subseteq {\mathrm{Base}}_{{W}}\wedge {U}\ne \varnothing \wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{x}{+}_{{W}}{y}\in {U}\wedge {inv}_{g}\left({W}\right)\left({x}\right)\in {U}\right)\right)\right)$
19 17 18 syl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to \left({U}\in \mathrm{SubGrp}\left({W}\right)↔\left({U}\subseteq {\mathrm{Base}}_{{W}}\wedge {U}\ne \varnothing \wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{x}{+}_{{W}}{y}\in {U}\wedge {inv}_{g}\left({W}\right)\left({x}\right)\in {U}\right)\right)\right)$
20 4 6 15 19 mpbir3and ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {U}\in \mathrm{SubGrp}\left({W}\right)$