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 21259
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 21256 . 2 class OBasis
2 vh . . 3 setvar β„Ž
3 cphl 21176 . . 3 class PreHil
4 vx . . . . . . . . . 10 setvar π‘₯
54cv 1540 . . . . . . . . 9 class π‘₯
6 vy . . . . . . . . . 10 setvar 𝑦
76cv 1540 . . . . . . . . 9 class 𝑦
82cv 1540 . . . . . . . . . 10 class β„Ž
9 cip 17201 . . . . . . . . . 10 class ·𝑖
108, 9cfv 6543 . . . . . . . . 9 class (Β·π‘–β€˜β„Ž)
115, 7, 10co 7408 . . . . . . . 8 class (π‘₯(Β·π‘–β€˜β„Ž)𝑦)
124, 6weq 1966 . . . . . . . . 9 wff π‘₯ = 𝑦
13 csca 17199 . . . . . . . . . . 11 class Scalar
148, 13cfv 6543 . . . . . . . . . 10 class (Scalarβ€˜β„Ž)
15 cur 20003 . . . . . . . . . 10 class 1r
1614, 15cfv 6543 . . . . . . . . 9 class (1rβ€˜(Scalarβ€˜β„Ž))
17 c0g 17384 . . . . . . . . . 10 class 0g
1814, 17cfv 6543 . . . . . . . . 9 class (0gβ€˜(Scalarβ€˜β„Ž))
1912, 16, 18cif 4528 . . . . . . . 8 class if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž)))
2011, 19wceq 1541 . . . . . . 7 wff (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž)))
21 vb . . . . . . . 8 setvar 𝑏
2221cv 1540 . . . . . . 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 21212 . . . . . . . 8 class ocv
268, 25cfv 6543 . . . . . . 7 class (ocvβ€˜β„Ž)
2722, 26cfv 6543 . . . . . 6 class ((ocvβ€˜β„Ž)β€˜π‘)
288, 17cfv 6543 . . . . . . 7 class (0gβ€˜β„Ž)
2928csn 4628 . . . . . 6 class {(0gβ€˜β„Ž)}
3027, 29wceq 1541 . . . . 5 wff ((ocvβ€˜β„Ž)β€˜π‘) = {(0gβ€˜β„Ž)}
3124, 30wa 396 . . . 4 wff (βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž))) ∧ ((ocvβ€˜β„Ž)β€˜π‘) = {(0gβ€˜β„Ž)})
32 cbs 17143 . . . . . 6 class Base
338, 32cfv 6543 . . . . 5 class (Baseβ€˜β„Ž)
3433cpw 4602 . . . 4 class 𝒫 (Baseβ€˜β„Ž)
3531, 21, 34crab 3432 . . 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 1541 1 wff OBasis = (β„Ž ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Baseβ€˜β„Ž) ∣ (βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž))) ∧ ((ocvβ€˜β„Ž)β€˜π‘) = {(0gβ€˜β„Ž)})})
Colors of variables: wff setvar class
This definition is referenced by:  isobs  21274
  Copyright terms: Public domain W3C validator