# 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}=\mathrm{Scalar}\left({W}\right)$
lssset.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
lssset.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lssset.p
lssset.t
lssset.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
Assertion islss

### Proof

Step Hyp Ref Expression
1 lssset.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
2 lssset.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
3 lssset.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
4 lssset.p
5 lssset.t
6 lssset.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
7 elfvex ${⊢}{U}\in \mathrm{LSubSp}\left({W}\right)\to {W}\in \mathrm{V}$
8 7 6 eleq2s ${⊢}{U}\in {S}\to {W}\in \mathrm{V}$
9 fvprc ${⊢}¬{W}\in \mathrm{V}\to {\mathrm{Base}}_{{W}}=\varnothing$
10 3 9 syl5eq ${⊢}¬{W}\in \mathrm{V}\to {V}=\varnothing$
11 10 sseq2d ${⊢}¬{W}\in \mathrm{V}\to \left({U}\subseteq {V}↔{U}\subseteq \varnothing \right)$
12 11 biimpcd ${⊢}{U}\subseteq {V}\to \left(¬{W}\in \mathrm{V}\to {U}\subseteq \varnothing \right)$
13 ss0 ${⊢}{U}\subseteq \varnothing \to {U}=\varnothing$
14 12 13 syl6 ${⊢}{U}\subseteq {V}\to \left(¬{W}\in \mathrm{V}\to {U}=\varnothing \right)$
15 14 necon1ad ${⊢}{U}\subseteq {V}\to \left({U}\ne \varnothing \to {W}\in \mathrm{V}\right)$
16 15 imp ${⊢}\left({U}\subseteq {V}\wedge {U}\ne \varnothing \right)\to {W}\in \mathrm{V}$
18 1 2 3 4 5 6 lssset
19 18 eleq2d
20 eldifsn ${⊢}{U}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)↔\left({U}\in 𝒫{V}\wedge {U}\ne \varnothing \right)$
21 3 fvexi ${⊢}{V}\in \mathrm{V}$
22 21 elpw2 ${⊢}{U}\in 𝒫{V}↔{U}\subseteq {V}$
23 22 anbi1i ${⊢}\left({U}\in 𝒫{V}\wedge {U}\ne \varnothing \right)↔\left({U}\subseteq {V}\wedge {U}\ne \varnothing \right)$
24 20 23 bitri ${⊢}{U}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)↔\left({U}\subseteq {V}\wedge {U}\ne \varnothing \right)$
25 24 anbi1i
26 eleq2
27 26 raleqbi1dv
28 27 raleqbi1dv
29 28 ralbidv
30 29 elrab
31 df-3an
32 25 30 31 3bitr4i
33 19 32 syl6bb
34 8 17 33 pm5.21nii