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 ‘ 𝑔 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑔 ) 𝑦 ) ) )