Metamath Proof Explorer


Theorem phlipf

Description: The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses ipffn.1 โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
ipffn.2 โŠข , = ( ยทif โ€˜ ๐‘Š )
phlipf.s โŠข ๐‘† = ( Scalar โ€˜ ๐‘Š )
phlipf.k โŠข ๐พ = ( Base โ€˜ ๐‘† )
Assertion phlipf ( ๐‘Š โˆˆ PreHil โ†’ , : ( ๐‘‰ ร— ๐‘‰ ) โŸถ ๐พ )

Proof

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 โ†’ , : ( ๐‘‰ ร— ๐‘‰ ) โŸถ ๐พ )