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 ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) ) )