lsssubg

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

		Ref	Expression
	Hypothesis	lsssubg.s	$⊢ S = LSubSp (W)$
	Assertion	lsssubg	$⊢ (W \in LMod \land U \in S) \to U \in SubGrp (W)$

Proof

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

Metamath Proof Explorer

Theorem lsssubg

Proof