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 20097
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 20094 . 2 class OBasis
2 vh . . 3 setvar
3 cphl 20017 . . 3 class PreHil
4 vx . . . . . . . . . 10 setvar 𝑥
54cv 1522 . . . . . . . . 9 class 𝑥
6 vy . . . . . . . . . 10 setvar 𝑦
76cv 1522 . . . . . . . . 9 class 𝑦
82cv 1522 . . . . . . . . . 10 class
9 cip 15993 . . . . . . . . . 10 class ·𝑖
108, 9cfv 5926 . . . . . . . . 9 class (·𝑖)
115, 7, 10co 6690 . . . . . . . 8 class (𝑥(·𝑖)𝑦)
124, 6weq 1931 . . . . . . . . 9 wff 𝑥 = 𝑦
13 csca 15991 . . . . . . . . . . 11 class Scalar
148, 13cfv 5926 . . . . . . . . . 10 class (Scalar‘)
15 cur 18547 . . . . . . . . . 10 class 1r
1614, 15cfv 5926 . . . . . . . . 9 class (1r‘(Scalar‘))
17 c0g 16147 . . . . . . . . . 10 class 0g
1814, 17cfv 5926 . . . . . . . . 9 class (0g‘(Scalar‘))
1912, 16, 18cif 4119 . . . . . . . 8 class if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2011, 19wceq 1523 . . . . . . 7 wff (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
21 vb . . . . . . . 8 setvar 𝑏
2221cv 1522 . . . . . . 7 class 𝑏
2320, 6, 22wral 2941 . . . . . 6 wff 𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2423, 4, 22wral 2941 . . . . 5 wff 𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
25 cocv 20052 . . . . . . . 8 class ocv
268, 25cfv 5926 . . . . . . 7 class (ocv‘)
2722, 26cfv 5926 . . . . . 6 class ((ocv‘)‘𝑏)
288, 17cfv 5926 . . . . . . 7 class (0g)
2928csn 4210 . . . . . 6 class {(0g)}
3027, 29wceq 1523 . . . . 5 wff ((ocv‘)‘𝑏) = {(0g)}
3124, 30wa 383 . . . 4 wff (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})
32 cbs 15904 . . . . . 6 class Base
338, 32cfv 5926 . . . . 5 class (Base‘)
3433cpw 4191 . . . 4 class 𝒫 (Base‘)
3531, 21, 34crab 2945 . . 3 class {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})}
362, 3, 35cmpt 4762 . 2 class ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
371, 36wceq 1523 1 wff OBasis = ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
Colors of variables: wff setvar class
This definition is referenced by:  isobs  20112
  Copyright terms: Public domain W3C validator