Step |
Hyp |
Ref |
Expression |
0 |
|
clsh |
|- LSHyp |
1 |
|
vw |
|- w |
2 |
|
cvv |
|- _V |
3 |
|
vs |
|- s |
4 |
|
clss |
|- LSubSp |
5 |
1
|
cv |
|- w |
6 |
5 4
|
cfv |
|- ( LSubSp ` w ) |
7 |
3
|
cv |
|- s |
8 |
|
cbs |
|- Base |
9 |
5 8
|
cfv |
|- ( Base ` w ) |
10 |
7 9
|
wne |
|- s =/= ( Base ` w ) |
11 |
|
vv |
|- v |
12 |
|
clspn |
|- LSpan |
13 |
5 12
|
cfv |
|- ( LSpan ` w ) |
14 |
11
|
cv |
|- v |
15 |
14
|
csn |
|- { v } |
16 |
7 15
|
cun |
|- ( s u. { v } ) |
17 |
16 13
|
cfv |
|- ( ( LSpan ` w ) ` ( s u. { v } ) ) |
18 |
17 9
|
wceq |
|- ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) |
19 |
18 11 9
|
wrex |
|- E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) |
20 |
10 19
|
wa |
|- ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) |
21 |
20 3 6
|
crab |
|- { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } |
22 |
1 2 21
|
cmpt |
|- ( w e. _V |-> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } ) |
23 |
0 22
|
wceq |
|- LSHyp = ( w e. _V |-> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } ) |