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

Definition df-obs 20374
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 20371 . 2 class OBasis
2 vh . . 3 setvar
3 cphl 20293 . . 3 class PreHil
4 vx . . . . . . . . . 10 setvar 𝑥
54cv 1652 . . . . . . . . 9 class 𝑥
6 vy . . . . . . . . . 10 setvar 𝑦
76cv 1652 . . . . . . . . 9 class 𝑦
82cv 1652 . . . . . . . . . 10 class
9 cip 16272 . . . . . . . . . 10 class ·𝑖
108, 9cfv 6101 . . . . . . . . 9 class (·𝑖)
115, 7, 10co 6878 . . . . . . . 8 class (𝑥(·𝑖)𝑦)
124, 6weq 2058 . . . . . . . . 9 wff 𝑥 = 𝑦
13 csca 16270 . . . . . . . . . . 11 class Scalar
148, 13cfv 6101 . . . . . . . . . 10 class (Scalar‘)
15 cur 18817 . . . . . . . . . 10 class 1r
1614, 15cfv 6101 . . . . . . . . 9 class (1r‘(Scalar‘))
17 c0g 16415 . . . . . . . . . 10 class 0g
1814, 17cfv 6101 . . . . . . . . 9 class (0g‘(Scalar‘))
1912, 16, 18cif 4277 . . . . . . . 8 class if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2011, 19wceq 1653 . . . . . . 7 wff (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
21 vb . . . . . . . 8 setvar 𝑏
2221cv 1652 . . . . . . 7 class 𝑏
2320, 6, 22wral 3089 . . . . . 6 wff 𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2423, 4, 22wral 3089 . . . . 5 wff 𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
25 cocv 20329 . . . . . . . 8 class ocv
268, 25cfv 6101 . . . . . . 7 class (ocv‘)
2722, 26cfv 6101 . . . . . 6 class ((ocv‘)‘𝑏)
288, 17cfv 6101 . . . . . . 7 class (0g)
2928csn 4368 . . . . . 6 class {(0g)}
3027, 29wceq 1653 . . . . 5 wff ((ocv‘)‘𝑏) = {(0g)}
3124, 30wa 385 . . . 4 wff (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})
32 cbs 16184 . . . . . 6 class Base
338, 32cfv 6101 . . . . 5 class (Base‘)
3433cpw 4349 . . . 4 class 𝒫 (Base‘)
3531, 21, 34crab 3093 . . 3 class {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})}
362, 3, 35cmpt 4922 . 2 class ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
371, 36wceq 1653 1 wff OBasis = ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
Colors of variables: wff setvar class
This definition is referenced by:  isobs  20389
  Copyright terms: Public domain W3C validator