ipcl

Description: Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	$⊢ F = Scalar (W)$
	phllmhm.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	phllmhm.v	$⊢ V = {Base}_{W}$
	ipcl.f	$⊢ K = {Base}_{F}$
Assertion	ipcl	$⊢ (W \in PreHil \land A \in V \land B \in V) \to A \underset{˙}{,} B \in K$

Step	Hyp	Ref	Expression
1		phlsrng.f	$⊢ F = Scalar (W)$
2		phllmhm.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		phllmhm.v	$⊢ V = {Base}_{W}$
4		ipcl.f	$⊢ K = {Base}_{F}$
5		eqid	$⊢ (x \in V ⟼ x \underset{˙}{,} B) = (x \in V ⟼ x \underset{˙}{,} B)$
6	1 2 3 5	phllmhm	$⊢ (W \in PreHil \land B \in V) \to (x \in V ⟼ x \underset{˙}{,} B) \in (W LMHom ringLMod (F))$
7		rlmbas	$⊢ {Base}_{F} = {Base}_{ringLMod (F)}$
8	4 7	eqtri	$⊢ K = {Base}_{ringLMod (F)}$
9	3 8	lmhmf	$⊢ (x \in V ⟼ x \underset{˙}{,} B) \in (W LMHom ringLMod (F)) \to (x \in V ⟼ x \underset{˙}{,} B) : V ⟶ K$
10	6 9	syl	$⊢ (W \in PreHil \land B \in V) \to (x \in V ⟼ x \underset{˙}{,} B) : V ⟶ K$
11	5	fmpt	$⊢ \forall x \in V x \underset{˙}{,} B \in K \leftrightarrow (x \in V ⟼ x \underset{˙}{,} B) : V ⟶ K$
12	10 11	sylibr	$⊢ (W \in PreHil \land B \in V) \to \forall x \in V x \underset{˙}{,} B \in K$
13		oveq1	$⊢ x = A \to x \underset{˙}{,} B = A \underset{˙}{,} B$
14	13	eleq1d	$⊢ x = A \to (x \underset{˙}{,} B \in K \leftrightarrow A \underset{˙}{,} B \in K)$
15	14	rspccva	$⊢ (\forall x \in V x \underset{˙}{,} B \in K \land A \in V) \to A \underset{˙}{,} B \in K$
16	12 15	stoic3	$⊢ (W \in PreHil \land B \in V \land A \in V) \to A \underset{˙}{,} B \in K$
17	16	3com23	$⊢ (W \in PreHil \land A \in V \land B \in V) \to A \underset{˙}{,} B \in K$

Metamath Proof Explorer