Theorem phlipf

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

	Ref	Expression
Hypotheses	ipffn.1	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ipffn.2	⊢ , = ( ·if ‘ 𝑊 )
	phlipf.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
	phlipf.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
Assertion	phlipf	⊢ ( 𝑊 ∈ PreHil → , : ( 𝑉 × 𝑉 ) ⟶ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		ipffn.1	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		ipffn.2	⊢ , = ( ·if ‘ 𝑊 )
3		phlipf.s	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
4		phlipf.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
5		eqid	⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
6	3 5 1 4	ipcl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 )
7	6	3expb	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 )
8	7	ralrimivva	⊢ ( 𝑊 ∈ PreHil → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 )
9	1 5 2	ipffval	⊢ , = ( 𝑥 ∈ 𝑉 , 𝑦 ∈ 𝑉 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) )
10	9	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ∈ 𝐾 ↔ , : ( 𝑉 × 𝑉 ) ⟶ 𝐾 )
11	8 10	sylib	⊢ ( 𝑊 ∈ PreHil → , : ( 𝑉 × 𝑉 ) ⟶ 𝐾 )