Step |
Hyp |
Ref |
Expression |
1 |
|
scaffval.b |
โข ๐ต = ( Base โ ๐ ) |
2 |
|
scaffval.f |
โข ๐น = ( Scalar โ ๐ ) |
3 |
|
scaffval.k |
โข ๐พ = ( Base โ ๐น ) |
4 |
|
scaffval.a |
โข โ = ( ยทsf โ ๐ ) |
5 |
|
scaffval.s |
โข ยท = ( ยท๐ โ ๐ ) |
6 |
1 2 3 4 5
|
scaffval |
โข โ = ( ๐ฅ โ ๐พ , ๐ฆ โ ๐ต โฆ ( ๐ฅ ยท ๐ฆ ) ) |
7 |
|
fnov |
โข ( ยท Fn ( ๐พ ร ๐ต ) โ ยท = ( ๐ฅ โ ๐พ , ๐ฆ โ ๐ต โฆ ( ๐ฅ ยท ๐ฆ ) ) ) |
8 |
7
|
biimpi |
โข ( ยท Fn ( ๐พ ร ๐ต ) โ ยท = ( ๐ฅ โ ๐พ , ๐ฆ โ ๐ต โฆ ( ๐ฅ ยท ๐ฆ ) ) ) |
9 |
6 8
|
eqtr4id |
โข ( ยท Fn ( ๐พ ร ๐ต ) โ โ = ยท ) |