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