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 e. LVec -> ( A e. ( ACS ` X ) /\ A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { 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 e. LVec -> W e. LMod )
5 3 1 lssacs
 |-  ( W e. LMod -> A e. ( ACS ` X ) )
6 4 5 syl
 |-  ( W e. LVec -> A e. ( ACS ` X ) )
7 simplll
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> W e. LVec )
8 simpllr
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> s e. ~P X )
9 8 elpwid
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> s C_ X )
10 simplr
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> y e. X )
11 simpr
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) )
12 eqid
 |-  ( LSpan ` W ) = ( LSpan ` W )
13 1 12 2 mrclsp
 |-  ( W e. LMod -> ( LSpan ` W ) = N )
14 7 4 13 3syl
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> ( LSpan ` W ) = N )
15 14 fveq1d
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> ( ( LSpan ` W ) ` ( s u. { y } ) ) = ( N ` ( s u. { y } ) ) )
16 14 fveq1d
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> ( ( LSpan ` W ) ` s ) = ( N ` s ) )
17 15 16 difeq12d
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> ( ( ( LSpan ` W ) ` ( s u. { y } ) ) \ ( ( LSpan ` W ) ` s ) ) = ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) )
18 11 17 eleqtrrd
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> z e. ( ( ( LSpan ` W ) ` ( s u. { y } ) ) \ ( ( LSpan ` W ) ` s ) ) )
19 3 1 12 lspsolv
 |-  ( ( W e. LVec /\ ( s C_ X /\ y e. X /\ z e. ( ( ( LSpan ` W ) ` ( s u. { y } ) ) \ ( ( LSpan ` W ) ` s ) ) ) ) -> y e. ( ( LSpan ` W ) ` ( s u. { z } ) ) )
20 7 9 10 18 19 syl13anc
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> y e. ( ( LSpan ` W ) ` ( s u. { z } ) ) )
21 14 fveq1d
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> ( ( LSpan ` W ) ` ( s u. { z } ) ) = ( N ` ( s u. { z } ) ) )
22 20 21 eleqtrd
 |-  ( ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) /\ z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) ) -> y e. ( N ` ( s u. { z } ) ) )
23 22 ralrimiva
 |-  ( ( ( W e. LVec /\ s e. ~P X ) /\ y e. X ) -> A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
24 23 ralrimiva
 |-  ( ( W e. LVec /\ s e. ~P X ) -> A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
25 24 ralrimiva
 |-  ( W e. LVec -> A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) )
26 6 25 jca
 |-  ( W e. LVec -> ( A e. ( ACS ` X ) /\ A. s e. ~P X A. y e. X A. z e. ( ( N ` ( s u. { y } ) ) \ ( N ` s ) ) y e. ( N ` ( s u. { z } ) ) ) )