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=BaseF
lssset.v ⊢V=BaseW
lssset.p ⊢+˙=+W
lssset.t ⊢·˙=⋅W
lssset.s ⊢S=LSubSp⁡W
Assertion islss ⊢U∈S↔U⊆V∧U≠∅∧∀x∈B∀a∈U∀b∈Ux·˙a+˙b∈U

Proof

Step Hyp Ref Expression
1 lssset.f ⊢F=Scalar⁡W
2 lssset.b ⊢B=BaseF
3 lssset.v ⊢V=BaseW
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→BaseW=∅
10 3 9 eqtrid ⊢¬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∈Ux·˙a+˙b∈U→W∈V
18 1 2 3 4 5 6 lssset ⊢W∈V→S=s∈𝒫V∖∅|∀x∈B∀a∈s∀b∈sx·˙a+˙b∈s
19 18 eleq2d ⊢W∈V→U∈S↔U∈s∈𝒫V∖∅|∀x∈B∀a∈s∀b∈sx·˙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∈Ux·˙a+˙b∈U↔U⊆V∧U≠∅∧∀x∈B∀a∈U∀b∈Ux·˙a+˙b∈U
26 eleq2 ⊢s=U→x·˙a+˙b∈s↔x·˙a+˙b∈U
27 26 raleqbi1dv ⊢s=U→∀b∈sx·˙a+˙b∈s↔∀b∈Ux·˙a+˙b∈U
28 27 raleqbi1dv ⊢s=U→∀a∈s∀b∈sx·˙a+˙b∈s↔∀a∈U∀b∈Ux·˙a+˙b∈U
29 28 ralbidv ⊢s=U→∀x∈B∀a∈s∀b∈sx·˙a+˙b∈s↔∀x∈B∀a∈U∀b∈Ux·˙a+˙b∈U
30 29 elrab ⊢U∈s∈𝒫V∖∅|∀x∈B∀a∈s∀b∈sx·˙a+˙b∈s↔U∈𝒫V∖∅∧∀x∈B∀a∈U∀b∈Ux·˙a+˙b∈U
31 df-3an ⊢U⊆V∧U≠∅∧∀x∈B∀a∈U∀b∈Ux·˙a+˙b∈U↔U⊆V∧U≠∅∧∀x∈B∀a∈U∀b∈Ux·˙a+˙b∈U
32 25 30 31 3bitr4i ⊢U∈s∈𝒫V∖∅|∀x∈B∀a∈s∀b∈sx·˙a+˙b∈s↔U⊆V∧U≠∅∧∀x∈B∀a∈U∀b∈Ux·˙a+˙b∈U
33 19 32 bitrdi ⊢W∈V→U∈S↔U⊆V∧U≠∅∧∀x∈B∀a∈U∀b∈Ux·˙a+˙b∈U
34 8 17 33 pm5.21nii ⊢U∈S↔U⊆V∧U≠∅∧∀x∈B∀a∈U∀b∈Ux·˙a+˙b∈U