phlipf

Description: The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Hypotheses	ipffn.1	$⊢ V = {Base}_{W}$
	ipffn.2	$⊢ \underset{˙}{,} = \cdot_{if} (W)$
	phlipf.s	$⊢ S = Scalar (W)$
	phlipf.k	$⊢ K = {Base}_{S}$
Assertion	phlipf	$⊢ W \in PreHil \to \underset{˙}{,} : V \times V ⟶ K$

Step	Hyp	Ref	Expression
1		ipffn.1	$⊢ V = {Base}_{W}$
2		ipffn.2	$⊢ \underset{˙}{,} = \cdot_{if} (W)$
3		phlipf.s	$⊢ S = Scalar (W)$
4		phlipf.k	$⊢ K = {Base}_{S}$
5		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
6	3 5 1 4	ipcl	$⊢ (W \in PreHil \land x \in V \land y \in V) \to x \cdot_{𝑖} (W) y \in K$
7	6	3expb	$⊢ (W \in PreHil \land (x \in V \land y \in V)) \to x \cdot_{𝑖} (W) y \in K$
8	7	ralrimivva	$⊢ W \in PreHil \to \forall x \in V \forall y \in V x \cdot_{𝑖} (W) y \in K$
9	1 5 2	ipffval	$⊢ \underset{˙}{,} = (x \in V, y \in V ⟼ x \cdot_{𝑖} (W) y)$
10	9	fmpo	$⊢ \forall x \in V \forall y \in V x \cdot_{𝑖} (W) y \in K \leftrightarrow \underset{˙}{,} : V \times V ⟶ K$
11	8 10	sylib	$⊢ W \in PreHil \to \underset{˙}{,} : V \times V ⟶ K$

Metamath Proof Explorer