Definition df-ipf 19972

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 19996), while ·_𝑖 only has closure (ipcl 19978). (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

Step	Hyp	Ref	Expression
1		cipf 19970	. 2 class ·if
2		vg	. . 3 setvar 𝑔
3		cvv 3200	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1482	. . . . 5 class 𝑔
7		cbs 15857	. . . . 5 class Base
8	6, 7	cfv 5888	. . . 4 class (Base‘𝑔)
9	4	cv 1482	. . . . 5 class 𝑥
10	5	cv 1482	. . . . 5 class 𝑦
11		cip 15946	. . . . . 6 class ·𝑖
12	6, 11	cfv 5888	. . . . 5 class (·𝑖‘𝑔)
13	9, 10, 12	co 6650	. . . 4 class (𝑥(·𝑖‘𝑔)𝑦)
14	4, 5, 8, 8, 13	cmpt2 6652	. . 3 class (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦))
15	2, 3, 14	cmpt 4729	. 2 class (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦)))
16	1, 15	wceq 1483	1 wff ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦)))

This definition is referenced by:  ipffval  19993