This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } ) ) ) )