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 20690
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 20714), while ·𝑖 only has closure (ipcl 20696). (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 20688 . 2 class ·if
2 vg . . 3 setvar 𝑔
3 cvv 3499 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1529 . . . . 5 class 𝑔
7 cbs 16476 . . . . 5 class Base
86, 7cfv 6351 . . . 4 class (Base‘𝑔)
94cv 1529 . . . . 5 class 𝑥
105cv 1529 . . . . 5 class 𝑦
11 cip 16563 . . . . . 6 class ·𝑖
126, 11cfv 6351 . . . . 5 class (·𝑖𝑔)
139, 10, 12co 7151 . . . 4 class (𝑥(·𝑖𝑔)𝑦)
144, 5, 8, 8, 13cmpo 7153 . . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦))
152, 3, 14cmpt 5142 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦)))
161, 15wceq 1530 1 wff ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦)))
Colors of variables: wff setvar class
This definition is referenced by:  ipffval  20711
  Copyright terms: Public domain W3C validator