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 20247
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 20271), while ·𝑖 only has closure (ipcl 20253). (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 20245 . 2 class ·if
2 vg . . 3 setvar 𝑔
3 cvv 3350 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1651 . . . . 5 class 𝑔
7 cbs 16130 . . . . 5 class Base
86, 7cfv 6068 . . . 4 class (Base‘𝑔)
94cv 1651 . . . . 5 class 𝑥
105cv 1651 . . . . 5 class 𝑦
11 cip 16219 . . . . . 6 class ·𝑖
126, 11cfv 6068 . . . . 5 class (·𝑖𝑔)
139, 10, 12co 6842 . . . 4 class (𝑥(·𝑖𝑔)𝑦)
144, 5, 8, 8, 13cmpt2 6844 . . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦))
152, 3, 14cmpt 4888 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦)))
161, 15wceq 1652 1 wff ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  ipffval  20268
  Copyright terms: Public domain W3C validator