Definition df-obs 21725

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

Step	Hyp	Ref	Expression
1		cobs 21722	. 2 class OBasis
2		vh	. . 3 setvar ℎ
3		cphl 21642	. . 3 class PreHil
4		vx	. . . . . . . . . 10 setvar 𝑥
5	4	cv 1539	. . . . . . . . 9 class 𝑥
6		vy	. . . . . . . . . 10 setvar 𝑦
7	6	cv 1539	. . . . . . . . 9 class 𝑦
8	2	cv 1539	. . . . . . . . . 10 class ℎ
9		cip 17302	. . . . . . . . . 10 class ·𝑖
10	8, 9	cfv 6561	. . . . . . . . 9 class (·𝑖‘ℎ)
11	5, 7, 10	co 7431	. . . . . . . 8 class (𝑥(·𝑖‘ℎ)𝑦)
12	4, 6	weq 1962	. . . . . . . . 9 wff 𝑥 = 𝑦
13		csca 17300	. . . . . . . . . . 11 class Scalar
14	8, 13	cfv 6561	. . . . . . . . . 10 class (Scalar‘ℎ)
15		cur 20178	. . . . . . . . . 10 class 1r
16	14, 15	cfv 6561	. . . . . . . . 9 class (1r‘(Scalar‘ℎ))
17		c0g 17484	. . . . . . . . . 10 class 0g
18	14, 17	cfv 6561	. . . . . . . . 9 class (0g‘(Scalar‘ℎ))
19	12, 16, 18	cif 4525	. . . . . . . 8 class if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
20	11, 19	wceq 1540	. . . . . . 7 wff (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
21		vb	. . . . . . . 8 setvar 𝑏
22	21	cv 1539	. . . . . . 7 class 𝑏
23	20, 6, 22	wral 3061	. . . . . 6 wff ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
24	23, 4, 22	wral 3061	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
25		cocv 21678	. . . . . . . 8 class ocv
26	8, 25	cfv 6561	. . . . . . 7 class (ocv‘ℎ)
27	22, 26	cfv 6561	. . . . . 6 class ((ocv‘ℎ)‘𝑏)
28	8, 17	cfv 6561	. . . . . . 7 class (0g‘ℎ)
29	28	csn 4626	. . . . . 6 class {(0g‘ℎ)}
30	27, 29	wceq 1540	. . . . 5 wff ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)}
31	24, 30	wa 395	. . . 4 wff (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})
32		cbs 17247	. . . . . 6 class Base
33	8, 32	cfv 6561	. . . . 5 class (Base‘ℎ)
34	33	cpw 4600	. . . 4 class 𝒫 (Base‘ℎ)
35	31, 21, 34	crab 3436	. . 3 class {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})}
36	2, 3, 35	cmpt 5225	. 2 class (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})})
37	1, 36	wceq 1540	1 wff OBasis = (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})})

This definition is referenced by:  isobs  21740