This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ipf

Description: Define the inner product function. Usually we will use .i 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 ), while .i only has closure ( ipcl ). (Contributed by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion df-ipf ⊢ ⋅ if = g ∈ V ⟼ x ∈ Base g , y ∈ Base g ⟼ x ⋅ 𝑖 ⁡ g y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cipf class ⋅ if
1 vg setvar g
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar g
6 5 4 cfv class Base g
7 vy setvar y
8 3 cv setvar x
9 cip class ⋅ 𝑖
10 5 9 cfv class ⋅ 𝑖 ⁡ g
11 7 cv setvar y
12 8 11 10 co class x ⋅ 𝑖 ⁡ g y
13 3 7 6 6 12 cmpo class x ∈ Base g , y ∈ Base g ⟼ x ⋅ 𝑖 ⁡ g y
14 1 2 13 cmpt class g ∈ V ⟼ x ∈ Base g , y ∈ Base g ⟼ x ⋅ 𝑖 ⁡ g y
15 0 14 wceq wff ⋅ if = g ∈ V ⟼ x ∈ Base g , y ∈ Base g ⟼ x ⋅ 𝑖 ⁡ g y