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 21260
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 21257 . 2 class OBasis
2 vh . . 3 setvar β„Ž
3 cphl 21177 . . 3 class PreHil
4 vx . . . . . . . . . 10 setvar π‘₯
54cv 1541 . . . . . . . . 9 class π‘₯
6 vy . . . . . . . . . 10 setvar 𝑦
76cv 1541 . . . . . . . . 9 class 𝑦
82cv 1541 . . . . . . . . . 10 class β„Ž
9 cip 17202 . . . . . . . . . 10 class ·𝑖
108, 9cfv 6544 . . . . . . . . 9 class (Β·π‘–β€˜β„Ž)
115, 7, 10co 7409 . . . . . . . 8 class (π‘₯(Β·π‘–β€˜β„Ž)𝑦)
124, 6weq 1967 . . . . . . . . 9 wff π‘₯ = 𝑦
13 csca 17200 . . . . . . . . . . 11 class Scalar
148, 13cfv 6544 . . . . . . . . . 10 class (Scalarβ€˜β„Ž)
15 cur 20004 . . . . . . . . . 10 class 1r
1614, 15cfv 6544 . . . . . . . . 9 class (1rβ€˜(Scalarβ€˜β„Ž))
17 c0g 17385 . . . . . . . . . 10 class 0g
1814, 17cfv 6544 . . . . . . . . 9 class (0gβ€˜(Scalarβ€˜β„Ž))
1912, 16, 18cif 4529 . . . . . . . 8 class if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž)))
2011, 19wceq 1542 . . . . . . 7 wff (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž)))
21 vb . . . . . . . 8 setvar 𝑏
2221cv 1541 . . . . . . 7 class 𝑏
2320, 6, 22wral 3062 . . . . . 6 wff βˆ€π‘¦ ∈ 𝑏 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž)))
2423, 4, 22wral 3062 . . . . 5 wff βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž)))
25 cocv 21213 . . . . . . . 8 class ocv
268, 25cfv 6544 . . . . . . 7 class (ocvβ€˜β„Ž)
2722, 26cfv 6544 . . . . . 6 class ((ocvβ€˜β„Ž)β€˜π‘)
288, 17cfv 6544 . . . . . . 7 class (0gβ€˜β„Ž)
2928csn 4629 . . . . . 6 class {(0gβ€˜β„Ž)}
3027, 29wceq 1542 . . . . 5 wff ((ocvβ€˜β„Ž)β€˜π‘) = {(0gβ€˜β„Ž)}
3124, 30wa 397 . . . 4 wff (βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž))) ∧ ((ocvβ€˜β„Ž)β€˜π‘) = {(0gβ€˜β„Ž)})
32 cbs 17144 . . . . . 6 class Base
338, 32cfv 6544 . . . . 5 class (Baseβ€˜β„Ž)
3433cpw 4603 . . . 4 class 𝒫 (Baseβ€˜β„Ž)
3531, 21, 34crab 3433 . . 3 class {𝑏 ∈ 𝒫 (Baseβ€˜β„Ž) ∣ (βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž))) ∧ ((ocvβ€˜β„Ž)β€˜π‘) = {(0gβ€˜β„Ž)})}
362, 3, 35cmpt 5232 . 2 class (β„Ž ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Baseβ€˜β„Ž) ∣ (βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž))) ∧ ((ocvβ€˜β„Ž)β€˜π‘) = {(0gβ€˜β„Ž)})})
371, 36wceq 1542 1 wff OBasis = (β„Ž ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Baseβ€˜β„Ž) ∣ (βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = if(π‘₯ = 𝑦, (1rβ€˜(Scalarβ€˜β„Ž)), (0gβ€˜(Scalarβ€˜β„Ž))) ∧ ((ocvβ€˜β„Ž)β€˜π‘) = {(0gβ€˜β„Ž)})})
Colors of variables: wff setvar class
This definition is referenced by:  isobs  21275
  Copyright terms: Public domain W3C validator