Metamath Proof Explorer

Theorem phllmhm

Description: The inner product of a pre-Hilbert space is linear in its left argument. (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}$
		phllmhm.g	$⊢ G = (x \in V ⟼ x \underset{˙}{,} A)$
	Assertion	phllmhm	$⊢ (W \in PreHil \land A \in V) \to G \in (W LMHom ringLMod (F))$

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	$⊢ F = Scalar (W)$
2		phllmhm.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		phllmhm.v	$⊢ V = {Base}_{W}$
4		phllmhm.g	$⊢ G = (x \in V ⟼ x \underset{˙}{,} A)$
5		eqid	$⊢ 0_{W} = 0_{W}$
6		eqid	$⊢ _{F} = _{F}$
7		eqid	$⊢ 0_{F} = 0_{F}$
8	3 1 2 5 6 7	isphl	$⊢ W \in PreHil \leftrightarrow (W \in LVec \land F \in -Ring \land \forall y \in V ((x \in V ⟼ x \underset{˙}{,} y) \in (W LMHom ringLMod (F)) \land (y \underset{˙}{,} y = 0_{F} \to y = 0_{W}) \land \forall x \in V {(y \underset{˙}{,} x)}^{_{F}} = x \underset{˙}{,} y))$
9	8	simp3bi	$⊢ W \in PreHil \to \forall y \in V ((x \in V ⟼ x \underset{˙}{,} y) \in (W LMHom ringLMod (F)) \land (y \underset{˙}{,} y = 0_{F} \to y = 0_{W}) \land \forall x \in V {(y \underset{˙}{,} x)}^{*_{F}} = x \underset{˙}{,} y)$
10		simp1	$⊢ ((x \in V ⟼ x \underset{˙}{,} y) \in (W LMHom ringLMod (F)) \land (y \underset{˙}{,} y = 0_{F} \to y = 0_{W}) \land \forall x \in V {(y \underset{˙}{,} x)}^{*_{F}} = x \underset{˙}{,} y) \to (x \in V ⟼ x \underset{˙}{,} y) \in (W LMHom ringLMod (F))$
11	10	ralimi	$⊢ \forall y \in V ((x \in V ⟼ x \underset{˙}{,} y) \in (W LMHom ringLMod (F)) \land (y \underset{˙}{,} y = 0_{F} \to y = 0_{W}) \land \forall x \in V {(y \underset{˙}{,} x)}^{*_{F}} = x \underset{˙}{,} y) \to \forall y \in V (x \in V ⟼ x \underset{˙}{,} y) \in (W LMHom ringLMod (F))$
12	9 11	syl	$⊢ W \in PreHil \to \forall y \in V (x \in V ⟼ x \underset{˙}{,} y) \in (W LMHom ringLMod (F))$
13		oveq2	$⊢ y = A \to x \underset{˙}{,} y = x \underset{˙}{,} A$
14	13	mpteq2dv	$⊢ y = A \to (x \in V ⟼ x \underset{˙}{,} y) = (x \in V ⟼ x \underset{˙}{,} A)$
15	14 4	eqtr4di	$⊢ y = A \to (x \in V ⟼ x \underset{˙}{,} y) = G$
16	15	eleq1d	$⊢ y = A \to ((x \in V ⟼ x \underset{˙}{,} y) \in (W LMHom ringLMod (F)) \leftrightarrow G \in (W LMHom ringLMod (F)))$
17	16	rspccva	$⊢ (\forall y \in V (x \in V ⟼ x \underset{˙}{,} y) \in (W LMHom ringLMod (F)) \land A \in V) \to G \in (W LMHom ringLMod (F))$
18	12 17	sylan	$⊢ (W \in PreHil \land A \in V) \to G \in (W LMHom ringLMod (F))$