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 20699
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 20723), while ·𝑖 only has closure (ipcl 20705). (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 20697 . 2 class ·if
2 vg . . 3 setvar 𝑔
3 cvv 3492 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1527 . . . . 5 class 𝑔
7 cbs 16471 . . . . 5 class Base
86, 7cfv 6348 . . . 4 class (Base‘𝑔)
94cv 1527 . . . . 5 class 𝑥
105cv 1527 . . . . 5 class 𝑦
11 cip 16558 . . . . . 6 class ·𝑖
126, 11cfv 6348 . . . . 5 class (·𝑖𝑔)
139, 10, 12co 7145 . . . 4 class (𝑥(·𝑖𝑔)𝑦)
144, 5, 8, 8, 13cmpo 7147 . . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦))
152, 3, 14cmpt 5137 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦)))
161, 15wceq 1528 1 wff ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  ipffval  20720
  Copyright terms: Public domain W3C validator