Metamath Proof Explorer


Theorem scafeq

Description: If the scalar multiplication operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses scaffval.b โŠข ๐ต = ( Base โ€˜ ๐‘Š )
scaffval.f โŠข ๐น = ( Scalar โ€˜ ๐‘Š )
scaffval.k โŠข ๐พ = ( Base โ€˜ ๐น )
scaffval.a โŠข โˆ™ = ( ยทsf โ€˜ ๐‘Š )
scaffval.s โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Š )
Assertion scafeq ( ยท Fn ( ๐พ ร— ๐ต ) โ†’ โˆ™ = ยท )

Proof

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 ( ๐พ ร— ๐ต ) โ†’ โˆ™ = ยท )