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 𝐴 = ( LSubSp ‘ 𝑊 )
lssacsex.2 𝑁 = ( mrCls ‘ 𝐴 )
lssacsex.3 𝑋 = ( Base ‘ 𝑊 )
Assertion lssacsex ( 𝑊 ∈ LVec → ( 𝐴 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) )

Proof

Step Hyp Ref Expression
1 lssacsex.1 𝐴 = ( LSubSp ‘ 𝑊 )
2 lssacsex.2 𝑁 = ( mrCls ‘ 𝐴 )
3 lssacsex.3 𝑋 = ( Base ‘ 𝑊 )
4 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
5 3 1 lssacs ( 𝑊 ∈ LMod → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
6 4 5 syl ( 𝑊 ∈ LVec → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
7 simplll ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → 𝑊 ∈ LVec )
8 simpllr ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → 𝑠 ∈ 𝒫 𝑋 )
9 8 elpwid ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → 𝑠𝑋 )
10 simplr ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → 𝑦𝑋 )
11 simpr ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) )
12 eqid ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
13 1 12 2 mrclsp ( 𝑊 ∈ LMod → ( LSpan ‘ 𝑊 ) = 𝑁 )
14 7 4 13 3syl ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → ( LSpan ‘ 𝑊 ) = 𝑁 )
15 14 fveq1d ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑦 } ) ) = ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) )
16 14 fveq1d ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ 𝑠 ) = ( 𝑁𝑠 ) )
17 15 16 difeq12d ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝑠 ) ) = ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) )
18 11 17 eleqtrrd ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → 𝑧 ∈ ( ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝑠 ) ) )
19 3 1 12 lspsolv ( ( 𝑊 ∈ LVec ∧ ( 𝑠𝑋𝑦𝑋𝑧 ∈ ( ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( ( LSpan ‘ 𝑊 ) ‘ 𝑠 ) ) ) ) → 𝑦 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
20 7 9 10 18 19 syl13anc ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → 𝑦 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
21 14 fveq1d ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑧 } ) ) = ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
22 20 21 eleqtrd ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) ∧ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) ) → 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
23 22 ralrimiva ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) ∧ 𝑦𝑋 ) → ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
24 23 ralrimiva ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝒫 𝑋 ) → ∀ 𝑦𝑋𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
25 24 ralrimiva ( 𝑊 ∈ LVec → ∀ 𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
26 6 25 jca ( 𝑊 ∈ LVec → ( 𝐴 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋𝑦𝑋𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) )