Step |
Hyp |
Ref |
Expression |
1 |
|
psrvsca.s |
โข ๐ = ( ๐ผ mPwSer ๐
) |
2 |
|
psrvsca.n |
โข โ = ( ยท๐ โ ๐ ) |
3 |
|
psrvsca.k |
โข ๐พ = ( Base โ ๐
) |
4 |
|
psrvsca.b |
โข ๐ต = ( Base โ ๐ ) |
5 |
|
psrvsca.m |
โข ยท = ( .r โ ๐
) |
6 |
|
psrvsca.d |
โข ๐ท = { โ โ ( โ0 โm ๐ผ ) โฃ ( โก โ โ โ ) โ Fin } |
7 |
|
psrvsca.x |
โข ( ๐ โ ๐ โ ๐พ ) |
8 |
|
psrvsca.y |
โข ( ๐ โ ๐น โ ๐ต ) |
9 |
|
sneq |
โข ( ๐ฅ = ๐ โ { ๐ฅ } = { ๐ } ) |
10 |
9
|
xpeq2d |
โข ( ๐ฅ = ๐ โ ( ๐ท ร { ๐ฅ } ) = ( ๐ท ร { ๐ } ) ) |
11 |
10
|
oveq1d |
โข ( ๐ฅ = ๐ โ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) = ( ( ๐ท ร { ๐ } ) โf ยท ๐ ) ) |
12 |
|
oveq2 |
โข ( ๐ = ๐น โ ( ( ๐ท ร { ๐ } ) โf ยท ๐ ) = ( ( ๐ท ร { ๐ } ) โf ยท ๐น ) ) |
13 |
1 2 3 4 5 6
|
psrvscafval |
โข โ = ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) |
14 |
|
ovex |
โข ( ( ๐ท ร { ๐ } ) โf ยท ๐น ) โ V |
15 |
11 12 13 14
|
ovmpo |
โข ( ( ๐ โ ๐พ โง ๐น โ ๐ต ) โ ( ๐ โ ๐น ) = ( ( ๐ท ร { ๐ } ) โf ยท ๐น ) ) |
16 |
7 8 15
|
syl2anc |
โข ( ๐ โ ( ๐ โ ๐น ) = ( ( ๐ท ร { ๐ } ) โf ยท ๐น ) ) |