Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-ipf | Structured version Visualization version GIF version |
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 19815), while ·𝑖 only has closure (ipcl 19797). (Contributed by Mario Carneiro, 12-Aug-2015.) |
Ref | Expression |
---|---|
df-ipf | ⊢ ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cipf 19789 | . 2 class ·if | |
2 | vg | . . 3 setvar 𝑔 | |
3 | cvv 3173 | . . 3 class V | |
4 | vx | . . . 4 setvar 𝑥 | |
5 | vy | . . . 4 setvar 𝑦 | |
6 | 2 | cv 1474 | . . . . 5 class 𝑔 |
7 | cbs 15695 | . . . . 5 class Base | |
8 | 6, 7 | cfv 5804 | . . . 4 class (Base‘𝑔) |
9 | 4 | cv 1474 | . . . . 5 class 𝑥 |
10 | 5 | cv 1474 | . . . . 5 class 𝑦 |
11 | cip 15773 | . . . . . 6 class ·𝑖 | |
12 | 6, 11 | cfv 5804 | . . . . 5 class (·𝑖‘𝑔) |
13 | 9, 10, 12 | co 6549 | . . . 4 class (𝑥(·𝑖‘𝑔)𝑦) |
14 | 4, 5, 8, 8, 13 | cmpt2 6551 | . . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦)) |
15 | 2, 3, 14 | cmpt 4643 | . 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦))) |
16 | 1, 15 | wceq 1475 | 1 wff ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦))) |
Colors of variables: wff setvar class |
This definition is referenced by: ipffval 19812 |
Copyright terms: Public domain | W3C validator |