Metamath Proof Explorer

Theorem islss

Description: The predicate "is a subspace" (of a left module or left vector space). (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypotheses lssset.f ⊢ F = Scalar ⁡ W
lssset.b ⊢ B = Base F
lssset.v ⊢ V = Base W
lssset.p ⊢ + ˙ = + W
lssset.t ⊢ · ˙ = ⋅ W
lssset.s ⊢ S = LSubSp ⁡ W
Assertion islss ⊢ U ∈ S ↔ U ⊆ V ∧ U ≠ ∅ ∧ ∀ x ∈ B ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U

Proof

Step Hyp Ref Expression
1 lssset.f ⊢ F = Scalar ⁡ W
2 lssset.b ⊢ B = Base F
3 lssset.v ⊢ V = Base W
4 lssset.p ⊢ + ˙ = + W
5 lssset.t ⊢ · ˙ = ⋅ W
6 lssset.s ⊢ S = LSubSp ⁡ W
7 elfvex ⊢ U ∈ LSubSp ⁡ W → W ∈ V
8 7 6 eleq2s ⊢ U ∈ S → W ∈ V
9 fvprc ⊢ ¬ W ∈ V → Base W = ∅
10 3 9 syl5eq ⊢ ¬ W ∈ V → V = ∅
11 10 sseq2d ⊢ ¬ W ∈ V → U ⊆ V ↔ U ⊆ ∅
12 11 biimpcd ⊢ U ⊆ V → ¬ W ∈ V → U ⊆ ∅
13 ss0 ⊢ U ⊆ ∅ → U = ∅
14 12 13 syl6 ⊢ U ⊆ V → ¬ W ∈ V → U = ∅
15 14 necon1ad ⊢ U ⊆ V → U ≠ ∅ → W ∈ V
16 15 imp ⊢ U ⊆ V ∧ U ≠ ∅ → W ∈ V
17 16 3adant3 ⊢ U ⊆ V ∧ U ≠ ∅ ∧ ∀ x ∈ B ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U → W ∈ V
18 1 2 3 4 5 6 lssset ⊢ W ∈ V → S = s ∈ 𝒫 V ∖ ∅ | ∀ x ∈ B ∀ a ∈ s ∀ b ∈ s x · ˙ a + ˙ b ∈ s
19 18 eleq2d ⊢ W ∈ V → U ∈ S ↔ U ∈ s ∈ 𝒫 V ∖ ∅ | ∀ x ∈ B ∀ a ∈ s ∀ b ∈ s x · ˙ a + ˙ b ∈ s
20 eldifsn ⊢ U ∈ 𝒫 V ∖ ∅ ↔ U ∈ 𝒫 V ∧ U ≠ ∅
21 3 fvexi ⊢ V ∈ V
22 21 elpw2 ⊢ U ∈ 𝒫 V ↔ U ⊆ V
23 22 anbi1i ⊢ U ∈ 𝒫 V ∧ U ≠ ∅ ↔ U ⊆ V ∧ U ≠ ∅
24 20 23 bitri ⊢ U ∈ 𝒫 V ∖ ∅ ↔ U ⊆ V ∧ U ≠ ∅
25 24 anbi1i ⊢ U ∈ 𝒫 V ∖ ∅ ∧ ∀ x ∈ B ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U ↔ U ⊆ V ∧ U ≠ ∅ ∧ ∀ x ∈ B ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U
26 eleq2 ⊢ s = U → x · ˙ a + ˙ b ∈ s ↔ x · ˙ a + ˙ b ∈ U
27 26 raleqbi1dv ⊢ s = U → ∀ b ∈ s x · ˙ a + ˙ b ∈ s ↔ ∀ b ∈ U x · ˙ a + ˙ b ∈ U
28 27 raleqbi1dv ⊢ s = U → ∀ a ∈ s ∀ b ∈ s x · ˙ a + ˙ b ∈ s ↔ ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U
29 28 ralbidv ⊢ s = U → ∀ x ∈ B ∀ a ∈ s ∀ b ∈ s x · ˙ a + ˙ b ∈ s ↔ ∀ x ∈ B ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U
30 29 elrab ⊢ U ∈ s ∈ 𝒫 V ∖ ∅ | ∀ x ∈ B ∀ a ∈ s ∀ b ∈ s x · ˙ a + ˙ b ∈ s ↔ U ∈ 𝒫 V ∖ ∅ ∧ ∀ x ∈ B ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U
31 df-3an ⊢ U ⊆ V ∧ U ≠ ∅ ∧ ∀ x ∈ B ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U ↔ U ⊆ V ∧ U ≠ ∅ ∧ ∀ x ∈ B ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U
32 25 30 31 3bitr4i ⊢ U ∈ s ∈ 𝒫 V ∖ ∅ | ∀ x ∈ B ∀ a ∈ s ∀ b ∈ s x · ˙ a + ˙ b ∈ s ↔ U ⊆ V ∧ U ≠ ∅ ∧ ∀ x ∈ B ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U
33 19 32 syl6bb ⊢ W ∈ V → U ∈ S ↔ U ⊆ V ∧ U ≠ ∅ ∧ ∀ x ∈ B ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U
34 8 17 33 pm5.21nii ⊢ U ∈ S ↔ U ⊆ V ∧ U ≠ ∅ ∧ ∀ x ∈ B ∀ a ∈ U ∀ b ∈ U x · ˙ a + ˙ b ∈ U