MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ipf Structured version   Visualization version   GIF version

Definition df-ipf 21054
Description: Define the inner product function. Usually we will use ยท๐‘– directly instead of ยทif, and they have the same behavior in most cases. The main advantage of ยทif is that it is a guaranteed function (ipffn 21078), while ยท๐‘– only has closure (ipcl 21060). (Contributed by Mario Carneiro, 12-Aug-2015.)
Assertion
Ref Expression
df-ipf ยทif = (๐‘” โˆˆ V โ†ฆ (๐‘ฅ โˆˆ (Baseโ€˜๐‘”), ๐‘ฆ โˆˆ (Baseโ€˜๐‘”) โ†ฆ (๐‘ฅ(ยท๐‘–โ€˜๐‘”)๐‘ฆ)))
Distinct variable group:   ๐‘ฅ,๐‘”,๐‘ฆ

Detailed syntax breakdown of Definition df-ipf
StepHypRef Expression
1 cipf 21052 . 2 class ยทif
2 vg . . 3 setvar ๐‘”
3 cvv 3447 . . 3 class V
4 vx . . . 4 setvar ๐‘ฅ
5 vy . . . 4 setvar ๐‘ฆ
62cv 1541 . . . . 5 class ๐‘”
7 cbs 17091 . . . . 5 class Base
86, 7cfv 6500 . . . 4 class (Baseโ€˜๐‘”)
94cv 1541 . . . . 5 class ๐‘ฅ
105cv 1541 . . . . 5 class ๐‘ฆ
11 cip 17146 . . . . . 6 class ยท๐‘–
126, 11cfv 6500 . . . . 5 class (ยท๐‘–โ€˜๐‘”)
139, 10, 12co 7361 . . . 4 class (๐‘ฅ(ยท๐‘–โ€˜๐‘”)๐‘ฆ)
144, 5, 8, 8, 13cmpo 7363 . . 3 class (๐‘ฅ โˆˆ (Baseโ€˜๐‘”), ๐‘ฆ โˆˆ (Baseโ€˜๐‘”) โ†ฆ (๐‘ฅ(ยท๐‘–โ€˜๐‘”)๐‘ฆ))
152, 3, 14cmpt 5192 . 2 class (๐‘” โˆˆ V โ†ฆ (๐‘ฅ โˆˆ (Baseโ€˜๐‘”), ๐‘ฆ โˆˆ (Baseโ€˜๐‘”) โ†ฆ (๐‘ฅ(ยท๐‘–โ€˜๐‘”)๐‘ฆ)))
161, 15wceq 1542 1 wff ยทif = (๐‘” โˆˆ V โ†ฆ (๐‘ฅ โˆˆ (Baseโ€˜๐‘”), ๐‘ฆ โˆˆ (Baseโ€˜๐‘”) โ†ฆ (๐‘ฅ(ยท๐‘–โ€˜๐‘”)๐‘ฆ)))
Colors of variables: wff setvar class
This definition is referenced by:  ipffval  21075
  Copyright terms: Public domain W3C validator