Step |
Hyp |
Ref |
Expression |
1 |
|
ipffn.1 |
โข ๐ = ( Base โ ๐ ) |
2 |
|
ipffn.2 |
โข , = ( ยทif โ ๐ ) |
3 |
|
phlipf.s |
โข ๐ = ( Scalar โ ๐ ) |
4 |
|
phlipf.k |
โข ๐พ = ( Base โ ๐ ) |
5 |
|
eqid |
โข ( ยท๐ โ ๐ ) = ( ยท๐ โ ๐ ) |
6 |
3 5 1 4
|
ipcl |
โข ( ( ๐ โ PreHil โง ๐ฅ โ ๐ โง ๐ฆ โ ๐ ) โ ( ๐ฅ ( ยท๐ โ ๐ ) ๐ฆ ) โ ๐พ ) |
7 |
6
|
3expb |
โข ( ( ๐ โ PreHil โง ( ๐ฅ โ ๐ โง ๐ฆ โ ๐ ) ) โ ( ๐ฅ ( ยท๐ โ ๐ ) ๐ฆ ) โ ๐พ ) |
8 |
7
|
ralrimivva |
โข ( ๐ โ PreHil โ โ ๐ฅ โ ๐ โ ๐ฆ โ ๐ ( ๐ฅ ( ยท๐ โ ๐ ) ๐ฆ ) โ ๐พ ) |
9 |
1 5 2
|
ipffval |
โข , = ( ๐ฅ โ ๐ , ๐ฆ โ ๐ โฆ ( ๐ฅ ( ยท๐ โ ๐ ) ๐ฆ ) ) |
10 |
9
|
fmpo |
โข ( โ ๐ฅ โ ๐ โ ๐ฆ โ ๐ ( ๐ฅ ( ยท๐ โ ๐ ) ๐ฆ ) โ ๐พ โ , : ( ๐ ร ๐ ) โถ ๐พ ) |
11 |
8 10
|
sylib |
โข ( ๐ โ PreHil โ , : ( ๐ ร ๐ ) โถ ๐พ ) |