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 = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( ·𝑖𝑔 ) 𝑦 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cipf ·if
1 vg 𝑔
2 cvv V
3 vx 𝑥
4 cbs Base
5 1 cv 𝑔
6 5 4 cfv ( Base ‘ 𝑔 )
7 vy 𝑦
8 3 cv 𝑥
9 cip ·𝑖
10 5 9 cfv ( ·𝑖𝑔 )
11 7 cv 𝑦
12 8 11 10 co ( 𝑥 ( ·𝑖𝑔 ) 𝑦 )
13 3 7 6 6 12 cmpo ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( ·𝑖𝑔 ) 𝑦 ) )
14 1 2 13 cmpt ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( ·𝑖𝑔 ) 𝑦 ) ) )
15 0 14 wceq ·if = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( ·𝑖𝑔 ) 𝑦 ) ) )