Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-obs | Structured version Visualization version Unicode version |
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 |
---|---|
df-obs | OBasis Scalar Scalar |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cobs 20046 | . 2 OBasis | |
2 | vh | . . 3 | |
3 | cphl 19969 | . . 3 | |
4 | vx | . . . . . . . . . 10 | |
5 | 4 | cv 1482 | . . . . . . . . 9 |
6 | vy | . . . . . . . . . 10 | |
7 | 6 | cv 1482 | . . . . . . . . 9 |
8 | 2 | cv 1482 | . . . . . . . . . 10 |
9 | cip 15946 | . . . . . . . . . 10 | |
10 | 8, 9 | cfv 5888 | . . . . . . . . 9 |
11 | 5, 7, 10 | co 6650 | . . . . . . . 8 |
12 | 4, 6 | weq 1874 | . . . . . . . . 9 |
13 | csca 15944 | . . . . . . . . . . 11 Scalar | |
14 | 8, 13 | cfv 5888 | . . . . . . . . . 10 Scalar |
15 | cur 18501 | . . . . . . . . . 10 | |
16 | 14, 15 | cfv 5888 | . . . . . . . . 9 Scalar |
17 | c0g 16100 | . . . . . . . . . 10 | |
18 | 14, 17 | cfv 5888 | . . . . . . . . 9 Scalar |
19 | 12, 16, 18 | cif 4086 | . . . . . . . 8 Scalar Scalar |
20 | 11, 19 | wceq 1483 | . . . . . . 7 Scalar Scalar |
21 | vb | . . . . . . . 8 | |
22 | 21 | cv 1482 | . . . . . . 7 |
23 | 20, 6, 22 | wral 2912 | . . . . . 6 Scalar Scalar |
24 | 23, 4, 22 | wral 2912 | . . . . 5 Scalar Scalar |
25 | cocv 20004 | . . . . . . . 8 | |
26 | 8, 25 | cfv 5888 | . . . . . . 7 |
27 | 22, 26 | cfv 5888 | . . . . . 6 |
28 | 8, 17 | cfv 5888 | . . . . . . 7 |
29 | 28 | csn 4177 | . . . . . 6 |
30 | 27, 29 | wceq 1483 | . . . . 5 |
31 | 24, 30 | wa 384 | . . . 4 Scalar Scalar |
32 | cbs 15857 | . . . . . 6 | |
33 | 8, 32 | cfv 5888 | . . . . 5 |
34 | 33 | cpw 4158 | . . . 4 |
35 | 31, 21, 34 | crab 2916 | . . 3 Scalar Scalar |
36 | 2, 3, 35 | cmpt 4729 | . 2 Scalar Scalar |
37 | 1, 36 | wceq 1483 | 1 OBasis Scalar Scalar |
Colors of variables: wff setvar class |
This definition is referenced by: isobs 20064 |
Copyright terms: Public domain | W3C validator |