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 e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( .i ` g ) y ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cipf	|- .if
1		vg	|- g
2		cvv	|- _V
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- g
6	5 4	cfv	|- ( Base ` g )
7		vy	|- y
8	3	cv	|- x
9		cip	|- .i
10	5 9	cfv	|- ( .i ` g )
11	7	cv	|- y
12	8 11 10	co	|- ( x ( .i ` g ) y )
13	3 7 6 6 12	cmpo	|- ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( .i ` g ) y ) )
14	1 2 13	cmpt	|- ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( .i ` g ) y ) ) )
15	0 14	wceq	|- .if = ( g e. _V |-> ( x e. ( Base ` g ) , y e. ( Base ` g ) |-> ( x ( .i ` g ) y ) ) )