isphl

Description: The predicate "is a generalized pre-Hilbert (inner product) space". (Contributed by NM, 22-Sep-2011) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	isphl.v	$⊢ V = {Base}_{W}$
	isphl.f	$⊢ F = Scalar (W)$
	isphl.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	isphl.o	$⊢ \underset{˙}{0} = 0_{W}$
	isphl.i	$⊢ \underset{˙}{} = _{F}$
	isphl.z	$⊢ Z = 0_{F}$
Assertion	isphl	$⊢ W \in PreHil \leftrightarrow (W \in LVec \land F \in -Ring \land \forall x \in V ((y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)) \land (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}) \land \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x))$

Proof

Step	Hyp	Ref	Expression
1		isphl.v	$⊢ V = {Base}_{W}$
2		isphl.f	$⊢ F = Scalar (W)$
3		isphl.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
4		isphl.o	$⊢ \underset{˙}{0} = 0_{W}$
5		isphl.i	$⊢ \underset{˙}{} = _{F}$
6		isphl.z	$⊢ Z = 0_{F}$
7		fvexd	$⊢ g = W \to {Base}_{g} \in V$
8		fvexd	$⊢ (g = W \land v = {Base}_{g}) \to \cdot_{𝑖} (g) \in V$
9		fvexd	$⊢ ((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \to Scalar (g) \in V$
10		id	$⊢ f = Scalar (g) \to f = Scalar (g)$
11		simpll	$⊢ ((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \to g = W$
12	11	fveq2d	$⊢ ((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \to Scalar (g) = Scalar (W)$
13	12 2	eqtr4di	$⊢ ((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \to Scalar (g) = F$
14	10 13	sylan9eqr	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to f = F$
15	14	eleq1d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to (f \in -Ring \leftrightarrow F \in -Ring)$
16		simpllr	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to v = {Base}_{g}$
17		simplll	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to g = W$
18	17	fveq2d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to {Base}_{g} = {Base}_{W}$
19	18 1	eqtr4di	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to {Base}_{g} = V$
20	16 19	eqtrd	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to v = V$
21		simplr	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to h = \cdot_{𝑖} (g)$
22	17	fveq2d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to \cdot_{𝑖} (g) = \cdot_{𝑖} (W)$
23	22 3	eqtr4di	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to \cdot_{𝑖} (g) = \underset{˙}{,}$
24	21 23	eqtrd	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to h = \underset{˙}{,}$
25	24	oveqd	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to y h x = y \underset{˙}{,} x$
26	20 25	mpteq12dv	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to (y \in v ⟼ y h x) = (y \in V ⟼ y \underset{˙}{,} x)$
27	14	fveq2d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to ringLMod (f) = ringLMod (F)$
28	17 27	oveq12d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to g LMHom ringLMod (f) = W LMHom ringLMod (F)$
29	26 28	eleq12d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to ((y \in v ⟼ y h x) \in (g LMHom ringLMod (f)) \leftrightarrow (y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)))$
30	24	oveqd	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to x h x = x \underset{˙}{,} x$
31	14	fveq2d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to 0_{f} = 0_{F}$
32	31 6	eqtr4di	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to 0_{f} = Z$
33	30 32	eqeq12d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to (x h x = 0_{f} \leftrightarrow x \underset{˙}{,} x = Z)$
34	17	fveq2d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to 0_{g} = 0_{W}$
35	34 4	eqtr4di	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to 0_{g} = \underset{˙}{0}$
36	35	eqeq2d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to (x = 0_{g} \leftrightarrow x = \underset{˙}{0})$
37	33 36	imbi12d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to ((x h x = 0_{f} \to x = 0_{g}) \leftrightarrow (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}))$
38	14	fveq2d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to _{f} = _{F}$
39	38 5	eqtr4di	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to _{f} = \underset{˙}{}$
40	24	oveqd	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to x h y = x \underset{˙}{,} y$
41	39 40	fveq12d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to {(x h y)}^{_{f}} = \underset{˙}{} (x \underset{˙}{,} y)$
42	41 25	eqeq12d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to ({(x h y)}^{_{f}} = y h x \leftrightarrow \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x)$
43	20 42	raleqbidv	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to (\forall y \in v {(x h y)}^{_{f}} = y h x \leftrightarrow \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x)$
44	29 37 43	3anbi123d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to (((y \in v ⟼ y h x) \in (g LMHom ringLMod (f)) \land (x h x = 0_{f} \to x = 0_{g}) \land \forall y \in v {(x h y)}^{_{f}} = y h x) \leftrightarrow ((y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)) \land (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}) \land \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x))$
45	20 44	raleqbidv	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to (\forall x \in v ((y \in v ⟼ y h x) \in (g LMHom ringLMod (f)) \land (x h x = 0_{f} \to x = 0_{g}) \land \forall y \in v {(x h y)}^{_{f}} = y h x) \leftrightarrow \forall x \in V ((y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)) \land (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}) \land \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x))$
46	15 45	anbi12d	$⊢ (((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \land f = Scalar (g)) \to ((f \in -Ring \land \forall x \in v ((y \in v ⟼ y h x) \in (g LMHom ringLMod (f)) \land (x h x = 0_{f} \to x = 0_{g}) \land \forall y \in v {(x h y)}^{_{f}} = y h x)) \leftrightarrow (F \in -Ring \land \forall x \in V ((y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)) \land (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}) \land \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x)))$
47	9 46	sbcied	$⊢ ((g = W \land v = {Base}_{g}) \land h = \cdot_{𝑖} (g)) \to (\underset{˙}{[} Scalar (g) / f \underset{˙}{]} (f \in -Ring \land \forall x \in v ((y \in v ⟼ y h x) \in (g LMHom ringLMod (f)) \land (x h x = 0_{f} \to x = 0_{g}) \land \forall y \in v {(x h y)}^{_{f}} = y h x)) \leftrightarrow (F \in -Ring \land \forall x \in V ((y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)) \land (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}) \land \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x)))$
48	8 47	sbcied	$⊢ (g = W \land v = {Base}_{g}) \to (\underset{˙}{[} \cdot_{𝑖} (g) / h \underset{˙}{]} \underset{˙}{[} Scalar (g) / f \underset{˙}{]} (f \in -Ring \land \forall x \in v ((y \in v ⟼ y h x) \in (g LMHom ringLMod (f)) \land (x h x = 0_{f} \to x = 0_{g}) \land \forall y \in v {(x h y)}^{_{f}} = y h x)) \leftrightarrow (F \in -Ring \land \forall x \in V ((y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)) \land (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}) \land \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x)))$
49	7 48	sbcied	$⊢ g = W \to (\underset{˙}{[} {Base}_{g} / v \underset{˙}{]} \underset{˙}{[} \cdot_{𝑖} (g) / h \underset{˙}{]} \underset{˙}{[} Scalar (g) / f \underset{˙}{]} (f \in -Ring \land \forall x \in v ((y \in v ⟼ y h x) \in (g LMHom ringLMod (f)) \land (x h x = 0_{f} \to x = 0_{g}) \land \forall y \in v {(x h y)}^{_{f}} = y h x)) \leftrightarrow (F \in -Ring \land \forall x \in V ((y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)) \land (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}) \land \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x)))$
50		df-phl	$⊢ PreHil = \{g \in LVec \| \underset{˙}{[} {Base}_{g} / v \underset{˙}{]} \underset{˙}{[} \cdot_{𝑖} (g) / h \underset{˙}{]} \underset{˙}{[} Scalar (g) / f \underset{˙}{]} (f \in -Ring \land \forall x \in v ((y \in v ⟼ y h x) \in (g LMHom ringLMod (f)) \land (x h x = 0_{f} \to x = 0_{g}) \land \forall y \in v {(x h y)}^{_{f}} = y h x))\}$
51	49 50	elrab2	$⊢ W \in PreHil \leftrightarrow (W \in LVec \land (F \in -Ring \land \forall x \in V ((y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)) \land (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}) \land \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x)))$
52		3anass	$⊢ (W \in LVec \land F \in -Ring \land \forall x \in V ((y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)) \land (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}) \land \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x)) \leftrightarrow (W \in LVec \land (F \in -Ring \land \forall x \in V ((y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)) \land (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}) \land \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x)))$
53	51 52	bitr4i	$⊢ W \in PreHil \leftrightarrow (W \in LVec \land F \in -Ring \land \forall x \in V ((y \in V ⟼ y \underset{˙}{,} x) \in (W LMHom ringLMod (F)) \land (x \underset{˙}{,} x = Z \to x = \underset{˙}{0}) \land \forall y \in V \underset{˙}{} (x \underset{˙}{,} y) = y \underset{˙}{,} x))$

Metamath Proof Explorer

Theorem isphl

Proof