Definition df-obs 21815

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 21812	. 2 class OBasis
2		vh	. . 3 setvar ℎ
3		cphl 21734	. . 3 class PreHil
4		vx	. . . . . . . . . 10 setvar 𝑥
5	4	cv 1562	. . . . . . . . 9 class 𝑥
6		vy	. . . . . . . . . 10 setvar 𝑦
7	6	cv 1562	. . . . . . . . 9 class 𝑦
8	2	cv 1562	. . . . . . . . . 10 class ℎ
9		cip 17305	. . . . . . . . . 10 class ·𝑖
10	8, 9	cfv 6525	. . . . . . . . 9 class (·𝑖‘ℎ)
11	5, 7, 10	co 7400	. . . . . . . 8 class (𝑥(·𝑖‘ℎ)𝑦)
12	4, 6	weq 1985	. . . . . . . . 9 wff 𝑥 = 𝑦
13		csca 17303	. . . . . . . . . . 11 class Scalar
14	8, 13	cfv 6525	. . . . . . . . . 10 class (Scalar‘ℎ)
15		cur 20254	. . . . . . . . . 10 class 1r
16	14, 15	cfv 6525	. . . . . . . . 9 class (1r‘(Scalar‘ℎ))
17		c0g 17482	. . . . . . . . . 10 class 0g
18	14, 17	cfv 6525	. . . . . . . . 9 class (0g‘(Scalar‘ℎ))
19	12, 16, 18	cif 4483	. . . . . . . 8 class if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
20	11, 19	wceq 1563	. . . . . . 7 wff (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
21		vb	. . . . . . . 8 setvar 𝑏
22	21	cv 1562	. . . . . . 7 class 𝑏
23	20, 6, 22	wral 3079	. . . . . 6 wff ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
24	23, 4, 22	wral 3079	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
25		cocv 21770	. . . . . . . 8 class ocv
26	8, 25	cfv 6525	. . . . . . 7 class (ocv‘ℎ)
27	22, 26	cfv 6525	. . . . . 6 class ((ocv‘ℎ)‘𝑏)
28	8, 17	cfv 6525	. . . . . . 7 class (0g‘ℎ)
29	28	csn 4585	. . . . . 6 class {(0g‘ℎ)}
30	27, 29	wceq 1563	. . . . 5 wff ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)}
31	24, 30	wa 400	. . . 4 wff (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})
32		cbs 17259	. . . . . 6 class Base
33	8, 32	cfv 6525	. . . . 5 class (Base‘ℎ)
34	33	cpw 4558	. . . 4 class 𝒫 (Base‘ℎ)
35	31, 21, 34	crab 3417	. . 3 class {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})}
36	2, 3, 35	cmpt 5186	. 2 class (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})})
37	1, 36	wceq 1563	1 wff OBasis = (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})})

This definition is referenced by:  isobs  21830