Metamath Proof Explorer

Theorem islss4

Description: A linear subspace is a subgroup which respects scalar multiplication. (Contributed by Stefan O'Rear, 11-Dec-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses islss4.f ⊢F=Scalar⁡W
islss4.b ⊢B=BaseF
islss4.v ⊢V=BaseW
islss4.t ⊢·˙=⋅W
islss4.s ⊢S=LSubSp⁡W
Assertion islss4 ⊢W∈LMod→U∈S↔U∈SubGrp⁡W∧∀a∈B∀b∈Ua·˙b∈U

Proof

Step Hyp Ref Expression
1 islss4.f ⊢F=Scalar⁡W
2 islss4.b ⊢B=BaseF
3 islss4.v ⊢V=BaseW
4 islss4.t ⊢·˙=⋅W
5 islss4.s ⊢S=LSubSp⁡W
6 5 lsssubg ⊢W∈LMod∧U∈S→U∈SubGrp⁡W
7 1 4 2 5 lssvscl ⊢W∈LMod∧U∈S∧a∈B∧b∈U→a·˙b∈U
8 7 ralrimivva ⊢W∈LMod∧U∈S→∀a∈B∀b∈Ua·˙b∈U
9 6 8 jca ⊢W∈LMod∧U∈S→U∈SubGrp⁡W∧∀a∈B∀b∈Ua·˙b∈U
10 3 subgss ⊢U∈SubGrp⁡W→U⊆V
11 10 ad2antrl ⊢W∈LMod∧U∈SubGrp⁡W∧∀a∈B∀b∈Ua·˙b∈U→U⊆V
12 eqid ⊢0W=0W
13 12 subg0cl ⊢U∈SubGrp⁡W→0W∈U
14 13 ne0d ⊢U∈SubGrp⁡W→U≠∅
15 14 ad2antrl ⊢W∈LMod∧U∈SubGrp⁡W∧∀a∈B∀b∈Ua·˙b∈U→U≠∅
16 eqid ⊢+W=+W
17 16 subgcl ⊢U∈SubGrp⁡W∧a·˙b∈U∧c∈U→a·˙b+Wc∈U
18 17 3exp ⊢U∈SubGrp⁡W→a·˙b∈U→c∈U→a·˙b+Wc∈U
19 18 adantl ⊢W∈LMod∧U∈SubGrp⁡W→a·˙b∈U→c∈U→a·˙b+Wc∈U
20 19 ralrimdv ⊢W∈LMod∧U∈SubGrp⁡W→a·˙b∈U→∀c∈Ua·˙b+Wc∈U
21 20 ralimdv ⊢W∈LMod∧U∈SubGrp⁡W→∀b∈Ua·˙b∈U→∀b∈U∀c∈Ua·˙b+Wc∈U
22 21 ralimdv ⊢W∈LMod∧U∈SubGrp⁡W→∀a∈B∀b∈Ua·˙b∈U→∀a∈B∀b∈U∀c∈Ua·˙b+Wc∈U
23 22 impr ⊢W∈LMod∧U∈SubGrp⁡W∧∀a∈B∀b∈Ua·˙b∈U→∀a∈B∀b∈U∀c∈Ua·˙b+Wc∈U
24 1 2 3 16 4 5 islss ⊢U∈S↔U⊆V∧U≠∅∧∀a∈B∀b∈U∀c∈Ua·˙b+Wc∈U
25 11 15 23 24 syl3anbrc ⊢W∈LMod∧U∈SubGrp⁡W∧∀a∈B∀b∈Ua·˙b∈U→U∈S
26 9 25 impbida ⊢W∈LMod→U∈S↔U∈SubGrp⁡W∧∀a∈B∀b∈Ua·˙b∈U