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	$$⊢{\cdot }_{\mathrm{if}}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{\cdot }_{𝑖}\left(g\right)y\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cipf	$$class{\cdot }_{\mathrm{if}}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarg$$
6	5 4	cfv	$$class{\mathrm{Base}}_g$$
7		vy	$$setvary$$
8	3	cv	$$setvarx$$
9		cip	$$class{\cdot }_{𝑖}$$
10	5 9	cfv	$$class{\cdot }_{𝑖}\left(g\right)$$
11	7	cv	$$setvary$$
12	8 11 10	co	$$class\left(x{\cdot }_{𝑖}\left(g\right)y\right)$$
13	3 7 6 6 12	cmpo	$$class\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{\cdot }_{𝑖}\left(g\right)y\right)$$
14	1 2 13	cmpt	$$class\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{\cdot }_{𝑖}\left(g\right)y\right)\right)$$
15	0 14	wceq	$$wff{\cdot }_{\mathrm{if}}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g,y\in {\mathrm{Base}}_g⟼x{\cdot }_{𝑖}\left(g\right)y\right)\right)$$