Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-obs Structured version   Visualization version   GIF version

Definition df-obs 19868
 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.)
Assertion
Ref Expression
df-obs OBasis = ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
Distinct variable group:   ,𝑏,𝑥,𝑦

Detailed syntax breakdown of Definition df-obs
StepHypRef Expression
1 cobs 19865 . 2 class OBasis
2 vh . . 3 setvar
3 cphl 19788 . . 3 class PreHil
4 vx . . . . . . . . . 10 setvar 𝑥
54cv 1474 . . . . . . . . 9 class 𝑥
6 vy . . . . . . . . . 10 setvar 𝑦
76cv 1474 . . . . . . . . 9 class 𝑦
82cv 1474 . . . . . . . . . 10 class
9 cip 15773 . . . . . . . . . 10 class ·𝑖
108, 9cfv 5804 . . . . . . . . 9 class (·𝑖)
115, 7, 10co 6549 . . . . . . . 8 class (𝑥(·𝑖)𝑦)
124, 6weq 1861 . . . . . . . . 9 wff 𝑥 = 𝑦
13 csca 15771 . . . . . . . . . . 11 class Scalar
148, 13cfv 5804 . . . . . . . . . 10 class (Scalar‘)
15 cur 18324 . . . . . . . . . 10 class 1r
1614, 15cfv 5804 . . . . . . . . 9 class (1r‘(Scalar‘))
17 c0g 15923 . . . . . . . . . 10 class 0g
1814, 17cfv 5804 . . . . . . . . 9 class (0g‘(Scalar‘))
1912, 16, 18cif 4036 . . . . . . . 8 class if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2011, 19wceq 1475 . . . . . . 7 wff (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
21 vb . . . . . . . 8 setvar 𝑏
2221cv 1474 . . . . . . 7 class 𝑏
2320, 6, 22wral 2896 . . . . . 6 wff 𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2423, 4, 22wral 2896 . . . . 5 wff 𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
25 cocv 19823 . . . . . . . 8 class ocv
268, 25cfv 5804 . . . . . . 7 class (ocv‘)
2722, 26cfv 5804 . . . . . 6 class ((ocv‘)‘𝑏)
288, 17cfv 5804 . . . . . . 7 class (0g)
2928csn 4125 . . . . . 6 class {(0g)}
3027, 29wceq 1475 . . . . 5 wff ((ocv‘)‘𝑏) = {(0g)}
3124, 30wa 383 . . . 4 wff (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})
32 cbs 15695 . . . . . 6 class Base
338, 32cfv 5804 . . . . 5 class (Base‘)
3433cpw 4108 . . . 4 class 𝒫 (Base‘)
3531, 21, 34crab 2900 . . 3 class {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})}
362, 3, 35cmpt 4643 . 2 class ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
371, 36wceq 1475 1 wff OBasis = ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
 Colors of variables: wff setvar class This definition is referenced by:  isobs  19883
 Copyright terms: Public domain W3C validator