df-phl

Description: Define the class of all pre-Hilbert spaces (inner product spaces) over arbitrary fields with involution. (Some textbook definitions are more restrictive and require the field of scalars to be the field of real or complex numbers). (Contributed by NM, 22-Sep-2011)

		Ref	Expression
	Assertion	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))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cphl	$class PreHil$
1		vg	$setvar g$
2		clvec	$class LVec$
3		cbs	$class Base$
4	1	cv	$setvar g$
5	4 3	cfv	$class {Base}_{g}$
6		vv	$setvar v$
7		cip	$class \cdot_{𝑖}$
8	4 7	cfv	$class \cdot_{𝑖} (g)$
9		vh	$setvar h$
10		csca	$class Scalar$
11	4 10	cfv	$class Scalar (g)$
12		vf	$setvar f$
13	12	cv	$setvar f$
14		csr	$class *-Ring$
15	13 14	wcel	$wff f \in *-Ring$
16		vx	$setvar x$
17	6	cv	$setvar v$
18		vy	$setvar y$
19	18	cv	$setvar y$
20	9	cv	$setvar h$
21	16	cv	$setvar x$
22	19 21 20	co	$class (y h x)$
23	18 17 22	cmpt	$class (y \in v ⟼ y h x)$
24		clmhm	$class LMHom$
25		crglmod	$class ringLMod$
26	13 25	cfv	$class ringLMod (f)$
27	4 26 24	co	$class (g LMHom ringLMod (f))$
28	23 27	wcel	$wff (y \in v ⟼ y h x) \in (g LMHom ringLMod (f))$
29	21 21 20	co	$class (x h x)$
30		c0g	$class 0_{𝑔}$
31	13 30	cfv	$class 0_{f}$
32	29 31	wceq	$wff x h x = 0_{f}$
33	4 30	cfv	$class 0_{g}$
34	21 33	wceq	$wff x = 0_{g}$
35	32 34	wi	$wff (x h x = 0_{f} \to x = 0_{g})$
36		cstv	$class *_{𝑟}$
37	13 36	cfv	$class *_{f}$
38	21 19 20	co	$class (x h y)$
39	38 37	cfv	$class {(x h y)}^{*_{f}}$
40	39 22	wceq	$wff {(x h y)}^{*_{f}} = y h x$
41	40 18 17	wral	$wff \forall y \in v {(x h y)}^{*_{f}} = y h x$
42	28 35 41	w3a	$wff ((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)$
43	42 16 17	wral	$wff \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)$
44	15 43	wa	$wff (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))$
45	44 12 11	wsbc	$wff \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))$
46	45 9 8	wsbc	$wff \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))$
47	46 6 5	wsbc	$wff \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))$
48	47 1 2	crab	$class \{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))\}$
49	0 48	wceq	$wff 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))\}$

Metamath Proof Explorer

Definition df-phl

Detailed syntax breakdown