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 21645
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 21669), while ·𝑖 only has closure (ipcl 21651). (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 21643 . 2 class ·if
2 vg . . 3 setvar 𝑔
3 cvv 3480 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1539 . . . . 5 class 𝑔
7 cbs 17247 . . . . 5 class Base
86, 7cfv 6561 . . . 4 class (Base‘𝑔)
94cv 1539 . . . . 5 class 𝑥
105cv 1539 . . . . 5 class 𝑦
11 cip 17302 . . . . . 6 class ·𝑖
126, 11cfv 6561 . . . . 5 class (·𝑖𝑔)
139, 10, 12co 7431 . . . 4 class (𝑥(·𝑖𝑔)𝑦)
144, 5, 8, 8, 13cmpo 7433 . . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦))
152, 3, 14cmpt 5225 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦)))
161, 15wceq 1540 1 wff ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  ipffval  21666
  Copyright terms: Public domain W3C validator