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 20266
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 20263 . 2 class OBasis
2 vh . . 3 setvar
3 cphl 20186 . . 3 class PreHil
4 vx . . . . . . . . . 10 setvar 𝑥
54cv 1630 . . . . . . . . 9 class 𝑥
6 vy . . . . . . . . . 10 setvar 𝑦
76cv 1630 . . . . . . . . 9 class 𝑦
82cv 1630 . . . . . . . . . 10 class
9 cip 16154 . . . . . . . . . 10 class ·𝑖
108, 9cfv 6030 . . . . . . . . 9 class (·𝑖)
115, 7, 10co 6796 . . . . . . . 8 class (𝑥(·𝑖)𝑦)
124, 6weq 2043 . . . . . . . . 9 wff 𝑥 = 𝑦
13 csca 16152 . . . . . . . . . . 11 class Scalar
148, 13cfv 6030 . . . . . . . . . 10 class (Scalar‘)
15 cur 18709 . . . . . . . . . 10 class 1r
1614, 15cfv 6030 . . . . . . . . 9 class (1r‘(Scalar‘))
17 c0g 16308 . . . . . . . . . 10 class 0g
1814, 17cfv 6030 . . . . . . . . 9 class (0g‘(Scalar‘))
1912, 16, 18cif 4226 . . . . . . . 8 class if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2011, 19wceq 1631 . . . . . . 7 wff (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
21 vb . . . . . . . 8 setvar 𝑏
2221cv 1630 . . . . . . 7 class 𝑏
2320, 6, 22wral 3061 . . . . . 6 wff 𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2423, 4, 22wral 3061 . . . . 5 wff 𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
25 cocv 20221 . . . . . . . 8 class ocv
268, 25cfv 6030 . . . . . . 7 class (ocv‘)
2722, 26cfv 6030 . . . . . 6 class ((ocv‘)‘𝑏)
288, 17cfv 6030 . . . . . . 7 class (0g)
2928csn 4317 . . . . . 6 class {(0g)}
3027, 29wceq 1631 . . . . 5 wff ((ocv‘)‘𝑏) = {(0g)}
3124, 30wa 382 . . . 4 wff (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})
32 cbs 16064 . . . . . 6 class Base
338, 32cfv 6030 . . . . 5 class (Base‘)
3433cpw 4298 . . . 4 class 𝒫 (Base‘)
3531, 21, 34crab 3065 . . 3 class {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})}
362, 3, 35cmpt 4864 . 2 class ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
371, 36wceq 1631 1 wff OBasis = ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
Colors of variables: wff setvar class
This definition is referenced by:  isobs  20281
  Copyright terms: Public domain W3C validator