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 20398
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 20395 . 2 class OBasis
2 vh . . 3 setvar
3 cphl 20317 . . 3 class PreHil
4 vx . . . . . . . . . 10 setvar 𝑥
54cv 1537 . . . . . . . . 9 class 𝑥
6 vy . . . . . . . . . 10 setvar 𝑦
76cv 1537 . . . . . . . . 9 class 𝑦
82cv 1537 . . . . . . . . . 10 class
9 cip 16566 . . . . . . . . . 10 class ·𝑖
108, 9cfv 6328 . . . . . . . . 9 class (·𝑖)
115, 7, 10co 7139 . . . . . . . 8 class (𝑥(·𝑖)𝑦)
124, 6weq 1964 . . . . . . . . 9 wff 𝑥 = 𝑦
13 csca 16564 . . . . . . . . . . 11 class Scalar
148, 13cfv 6328 . . . . . . . . . 10 class (Scalar‘)
15 cur 19248 . . . . . . . . . 10 class 1r
1614, 15cfv 6328 . . . . . . . . 9 class (1r‘(Scalar‘))
17 c0g 16709 . . . . . . . . . 10 class 0g
1814, 17cfv 6328 . . . . . . . . 9 class (0g‘(Scalar‘))
1912, 16, 18cif 4428 . . . . . . . 8 class if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2011, 19wceq 1538 . . . . . . 7 wff (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
21 vb . . . . . . . 8 setvar 𝑏
2221cv 1537 . . . . . . 7 class 𝑏
2320, 6, 22wral 3109 . . . . . 6 wff 𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
2423, 4, 22wral 3109 . . . . 5 wff 𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘)))
25 cocv 20353 . . . . . . . 8 class ocv
268, 25cfv 6328 . . . . . . 7 class (ocv‘)
2722, 26cfv 6328 . . . . . 6 class ((ocv‘)‘𝑏)
288, 17cfv 6328 . . . . . . 7 class (0g)
2928csn 4528 . . . . . 6 class {(0g)}
3027, 29wceq 1538 . . . . 5 wff ((ocv‘)‘𝑏) = {(0g)}
3124, 30wa 399 . . . 4 wff (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})
32 cbs 16479 . . . . . 6 class Base
338, 32cfv 6328 . . . . 5 class (Base‘)
3433cpw 4500 . . . 4 class 𝒫 (Base‘)
3531, 21, 34crab 3113 . . 3 class {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})}
362, 3, 35cmpt 5113 . 2 class ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
371, 36wceq 1538 1 wff OBasis = ( ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘) ∣ (∀𝑥𝑏𝑦𝑏 (𝑥(·𝑖)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘)), (0g‘(Scalar‘))) ∧ ((ocv‘)‘𝑏) = {(0g)})})
Colors of variables: wff setvar class
This definition is referenced by:  isobs  20413
  Copyright terms: Public domain W3C validator