Step |
Hyp |
Ref |
Expression |
0 |
|
cresv |
⊢ ↾v |
1 |
|
vw |
⊢ 𝑤 |
2 |
|
cvv |
⊢ V |
3 |
|
vx |
⊢ 𝑥 |
4 |
|
cbs |
⊢ Base |
5 |
|
csca |
⊢ Scalar |
6 |
1
|
cv |
⊢ 𝑤 |
7 |
6 5
|
cfv |
⊢ ( Scalar ‘ 𝑤 ) |
8 |
7 4
|
cfv |
⊢ ( Base ‘ ( Scalar ‘ 𝑤 ) ) |
9 |
3
|
cv |
⊢ 𝑥 |
10 |
8 9
|
wss |
⊢ ( Base ‘ ( Scalar ‘ 𝑤 ) ) ⊆ 𝑥 |
11 |
|
csts |
⊢ sSet |
12 |
|
cnx |
⊢ ndx |
13 |
12 5
|
cfv |
⊢ ( Scalar ‘ ndx ) |
14 |
|
cress |
⊢ ↾s |
15 |
7 9 14
|
co |
⊢ ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) |
16 |
13 15
|
cop |
⊢ 〈 ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) 〉 |
17 |
6 16 11
|
co |
⊢ ( 𝑤 sSet 〈 ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) 〉 ) |
18 |
10 6 17
|
cif |
⊢ if ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ⊆ 𝑥 , 𝑤 , ( 𝑤 sSet 〈 ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) 〉 ) ) |
19 |
1 3 2 2 18
|
cmpo |
⊢ ( 𝑤 ∈ V , 𝑥 ∈ V ↦ if ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ⊆ 𝑥 , 𝑤 , ( 𝑤 sSet 〈 ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) 〉 ) ) ) |
20 |
0 19
|
wceq |
⊢ ↾v = ( 𝑤 ∈ V , 𝑥 ∈ V ↦ if ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ⊆ 𝑥 , 𝑤 , ( 𝑤 sSet 〈 ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑤 ) ↾s 𝑥 ) 〉 ) ) ) |