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

Definition df-ipf 20338
 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 20362), while ·𝑖 only has closure (ipcl 20344). (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 20336 . 2 class ·if
2 vg . . 3 setvar 𝑔
3 cvv 3442 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1537 . . . . 5 class 𝑔
7 cbs 16495 . . . . 5 class Base
86, 7cfv 6332 . . . 4 class (Base‘𝑔)
94cv 1537 . . . . 5 class 𝑥
105cv 1537 . . . . 5 class 𝑦
11 cip 16582 . . . . . 6 class ·𝑖
126, 11cfv 6332 . . . . 5 class (·𝑖𝑔)
139, 10, 12co 7145 . . . 4 class (𝑥(·𝑖𝑔)𝑦)
144, 5, 8, 8, 13cmpo 7147 . . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦))
152, 3, 14cmpt 5114 . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦)))
161, 15wceq 1538 1 wff ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖𝑔)𝑦)))
 Colors of variables: wff setvar class This definition is referenced by:  ipffval  20359
 Copyright terms: Public domain W3C validator