Step |
Hyp |
Ref |
Expression |
0 |
|
clsh |
⊢ LSHyp |
1 |
|
vw |
⊢ 𝑤 |
2 |
|
cvv |
⊢ V |
3 |
|
vs |
⊢ 𝑠 |
4 |
|
clss |
⊢ LSubSp |
5 |
1
|
cv |
⊢ 𝑤 |
6 |
5 4
|
cfv |
⊢ ( LSubSp ‘ 𝑤 ) |
7 |
3
|
cv |
⊢ 𝑠 |
8 |
|
cbs |
⊢ Base |
9 |
5 8
|
cfv |
⊢ ( Base ‘ 𝑤 ) |
10 |
7 9
|
wne |
⊢ 𝑠 ≠ ( Base ‘ 𝑤 ) |
11 |
|
vv |
⊢ 𝑣 |
12 |
|
clspn |
⊢ LSpan |
13 |
5 12
|
cfv |
⊢ ( LSpan ‘ 𝑤 ) |
14 |
11
|
cv |
⊢ 𝑣 |
15 |
14
|
csn |
⊢ { 𝑣 } |
16 |
7 15
|
cun |
⊢ ( 𝑠 ∪ { 𝑣 } ) |
17 |
16 13
|
cfv |
⊢ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) |
18 |
17 9
|
wceq |
⊢ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) |
19 |
18 11 9
|
wrex |
⊢ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) |
20 |
10 19
|
wa |
⊢ ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ) |
21 |
20 3 6
|
crab |
⊢ { 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ∣ ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ) } |
22 |
1 2 21
|
cmpt |
⊢ ( 𝑤 ∈ V ↦ { 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ∣ ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ) } ) |
23 |
0 22
|
wceq |
⊢ LSHyp = ( 𝑤 ∈ V ↦ { 𝑠 ∈ ( LSubSp ‘ 𝑤 ) ∣ ( 𝑠 ≠ ( Base ‘ 𝑤 ) ∧ ∃ 𝑣 ∈ ( Base ‘ 𝑤 ) ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = ( Base ‘ 𝑤 ) ) } ) |