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 21743
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 21740 . 2 class OBasis
2 vh . . 3 setvar
3 cphl 21660 . . 3 class PreHil
4 vx . . . . . . . . . 10 setvar 𝑥
54cv 1536 . . . . . . . . 9 class 𝑥
6 vy . . . . . . . . . 10 setvar 𝑦
76cv 1536 . . . . . . . . 9 class 𝑦
82cv 1536 . . . . . . . . . 10 class
9 cip 17303 . . . . . . . . . 10 class ·𝑖
108, 9cfv 6563 . . . . . . . . 9 class (·𝑖)
115, 7, 10co 7431 . . . . . . . 8 class (𝑥(·𝑖)𝑦)
124, 6weq 1960 . . . . . . . . 9 wff 𝑥 = 𝑦
13 csca 17301 . . . . . . . . . . 11 class Scalar
148, 13cfv 6563 . . . . . . . . . 10 class (Scalar‘)
15 cur 20199 . . . . . . . . . 10 class 1r
1614, 15cfv 6563 . . . . . . . . 9 class (1r‘(Scalar‘))
17 c0g 17486 . . . . . . . . . 10 class 0g
1814, 17cfv 6563 . . . . . . . . 9 class (0g‘(Scalar‘))
1912, 16, 18cif 4531 . . . . . . . 8 class if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2011, 19wceq 1537 . . . . . . 7 wff (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
21 vb . . . . . . . 8 setvar 𝑏
2221cv 1536 . . . . . . 7 class 𝑏
2320, 6, 22wral 3059 . . . . . 6 wff 𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2423, 4, 22wral 3059 . . . . 5 wff 𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
25 cocv 21696 . . . . . . . 8 class ocv
268, 25cfv 6563 . . . . . . 7 class (ocv‘)
2722, 26cfv 6563 . . . . . 6 class ((ocv‘)‘𝑏)
288, 17cfv 6563 . . . . . . 7 class (0g)
2928csn 4631 . . . . . 6 class {(0g)}
3027, 29wceq 1537 . . . . 5 wff ((ocv‘)‘𝑏) = {(0g)}
3124, 30wa 395 . . . 4 wff (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})
32 cbs 17245 . . . . . 6 class Base
338, 32cfv 6563 . . . . 5 class (Base‘)
3433cpw 4605 . . . 4 class 𝒫 (Base‘)
3531, 21, 34crab 3433 . . 3 class {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})}
362, 3, 35cmpt 5231 . 2 class ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
371, 36wceq 1537 1 wff OBasis = ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
Colors of variables: wff setvar class
This definition is referenced by:  isobs  21758
  Copyright terms: Public domain W3C validator