Metamath Proof Explorer


Theorem lssacsex

Description: In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs by lspsolv . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses lssacsex.1 A = LSubSp W
lssacsex.2 N = mrCls A
lssacsex.3 X = Base W
Assertion lssacsex W LVec A ACS X s 𝒫 X y X z N s y N s y N s z

Proof

Step Hyp Ref Expression
1 lssacsex.1 A = LSubSp W
2 lssacsex.2 N = mrCls A
3 lssacsex.3 X = Base W
4 lveclmod W LVec W LMod
5 3 1 lssacs W LMod A ACS X
6 4 5 syl W LVec A ACS X
7 simplll W LVec s 𝒫 X y X z N s y N s W LVec
8 simpllr W LVec s 𝒫 X y X z N s y N s s 𝒫 X
9 8 elpwid W LVec s 𝒫 X y X z N s y N s s X
10 simplr W LVec s 𝒫 X y X z N s y N s y X
11 simpr W LVec s 𝒫 X y X z N s y N s z N s y N s
12 eqid LSpan W = LSpan W
13 1 12 2 mrclsp W LMod LSpan W = N
14 7 4 13 3syl W LVec s 𝒫 X y X z N s y N s LSpan W = N
15 14 fveq1d W LVec s 𝒫 X y X z N s y N s LSpan W s y = N s y
16 14 fveq1d W LVec s 𝒫 X y X z N s y N s LSpan W s = N s
17 15 16 difeq12d W LVec s 𝒫 X y X z N s y N s LSpan W s y LSpan W s = N s y N s
18 11 17 eleqtrrd W LVec s 𝒫 X y X z N s y N s z LSpan W s y LSpan W s
19 3 1 12 lspsolv W LVec s X y X z LSpan W s y LSpan W s y LSpan W s z
20 7 9 10 18 19 syl13anc W LVec s 𝒫 X y X z N s y N s y LSpan W s z
21 14 fveq1d W LVec s 𝒫 X y X z N s y N s LSpan W s z = N s z
22 20 21 eleqtrd W LVec s 𝒫 X y X z N s y N s y N s z
23 22 ralrimiva W LVec s 𝒫 X y X z N s y N s y N s z
24 23 ralrimiva W LVec s 𝒫 X y X z N s y N s y N s z
25 24 ralrimiva W LVec s 𝒫 X y X z N s y N s y N s z
26 6 25 jca W LVec A ACS X s 𝒫 X y X z N s y N s y N s z