Metamath Proof Explorer

Definition df-obs

Description: Define the set of all orthonormal bases for a pre-Hilbert space. An orthonormal basis is a set of mutually orthogonal vectors with norm 1 and such that the linear span is dense in the whole space. (As this is an "algebraic" definition, before we have topology available, we express this denseness by saying that the double orthocomplement is the whole space, or equivalently, the single orthocomplement is trivial.) (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Assertion df-obs ⊢OBasis=h∈PreHil⟼b∈𝒫Baseh|∀x∈b∀y∈bx⋅𝑖⁡hy=ifx=y1Scalar⁡h0Scalar⁡h∧ocv⁡h⁡b=0h

Detailed syntax breakdown

Step Hyp Ref Expression
0 cobs classOBasis
1 vh setvarh
2 cphl classPreHil
3 vb setvarb
4 cbs classBase
5 1 cv setvarh
6 5 4 cfv classBaseh
7 6 cpw class𝒫Baseh
8 vx setvarx
9 3 cv setvarb
10 vy setvary
11 8 cv setvarx
12 cip class⋅𝑖
13 5 12 cfv class⋅𝑖⁡h
14 10 cv setvary
15 11 14 13 co classx⋅𝑖⁡hy
16 11 14 wceq wffx=y
17 cur class1r
18 csca classScalar
19 5 18 cfv classScalar⁡h
20 19 17 cfv class1Scalar⁡h
21 c0g class0𝑔
22 19 21 cfv class0Scalar⁡h
23 16 20 22 cif classifx=y1Scalar⁡h0Scalar⁡h
24 15 23 wceq wffx⋅𝑖⁡hy=ifx=y1Scalar⁡h0Scalar⁡h
25 24 10 9 wral wff∀y∈bx⋅𝑖⁡hy=ifx=y1Scalar⁡h0Scalar⁡h
26 25 8 9 wral wff∀x∈b∀y∈bx⋅𝑖⁡hy=ifx=y1Scalar⁡h0Scalar⁡h
27 cocv classocv
28 5 27 cfv classocv⁡h
29 9 28 cfv classocv⁡h⁡b
30 5 21 cfv class0h
31 30 csn class0h
32 29 31 wceq wffocv⁡h⁡b=0h
33 26 32 wa wff∀x∈b∀y∈bx⋅𝑖⁡hy=ifx=y1Scalar⁡h0Scalar⁡h∧ocv⁡h⁡b=0h
34 33 3 7 crab classb∈𝒫Baseh|∀x∈b∀y∈bx⋅𝑖⁡hy=ifx=y1Scalar⁡h0Scalar⁡h∧ocv⁡h⁡b=0h
35 1 2 34 cmpt classh∈PreHil⟼b∈𝒫Baseh|∀x∈b∀y∈bx⋅𝑖⁡hy=ifx=y1Scalar⁡h0Scalar⁡h∧ocv⁡h⁡b=0h
36 0 35 wceq wffOBasis=h∈PreHil⟼b∈𝒫Baseh|∀x∈b∀y∈bx⋅𝑖⁡hy=ifx=y1Scalar⁡h0Scalar⁡h∧ocv⁡h⁡b=0h