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 = Base F
islss4.v ⊢ V = Base W
islss4.t ⊢ · ˙ = ⋅ W
islss4.s ⊢ S = LSubSp ⁡ W
Assertion islss4 ⊢ W ∈ LMod → U ∈ S ↔ U ∈ SubGrp ⁡ W ∧ ∀ a ∈ B ∀ b ∈ U a · ˙ b ∈ U

Proof

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