Definition df-obs 21737

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 21734	. 2 class OBasis
2		vh	. . 3 setvar ℎ
3		cphl 21656	. . 3 class PreHil
4		vx	. . . . . . . . . 10 setvar 𝑥
5	4	cv 1558	. . . . . . . . 9 class 𝑥
6		vy	. . . . . . . . . 10 setvar 𝑦
7	6	cv 1558	. . . . . . . . 9 class 𝑦
8	2	cv 1558	. . . . . . . . . 10 class ℎ
9		cip 17274	. . . . . . . . . 10 class ·𝑖
10	8, 9	cfv 6517	. . . . . . . . 9 class (·𝑖‘ℎ)
11	5, 7, 10	co 7392	. . . . . . . 8 class (𝑥(·𝑖‘ℎ)𝑦)
12	4, 6	weq 1981	. . . . . . . . 9 wff 𝑥 = 𝑦
13		csca 17272	. . . . . . . . . . 11 class Scalar
14	8, 13	cfv 6517	. . . . . . . . . 10 class (Scalar‘ℎ)
15		cur 20210	. . . . . . . . . 10 class 1r
16	14, 15	cfv 6517	. . . . . . . . 9 class (1r‘(Scalar‘ℎ))
17		c0g 17451	. . . . . . . . . 10 class 0g
18	14, 17	cfv 6517	. . . . . . . . 9 class (0g‘(Scalar‘ℎ))
19	12, 16, 18	cif 4479	. . . . . . . 8 class if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
20	11, 19	wceq 1559	. . . . . . 7 wff (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
21		vb	. . . . . . . 8 setvar 𝑏
22	21	cv 1558	. . . . . . 7 class 𝑏
23	20, 6, 22	wral 3075	. . . . . 6 wff ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
24	23, 4, 22	wral 3075	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
25		cocv 21692	. . . . . . . 8 class ocv
26	8, 25	cfv 6517	. . . . . . 7 class (ocv‘ℎ)
27	22, 26	cfv 6517	. . . . . 6 class ((ocv‘ℎ)‘𝑏)
28	8, 17	cfv 6517	. . . . . . 7 class (0g‘ℎ)
29	28	csn 4581	. . . . . 6 class {(0g‘ℎ)}
30	27, 29	wceq 1559	. . . . 5 wff ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)}
31	24, 30	wa 399	. . . 4 wff (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})
32		cbs 17228	. . . . . 6 class Base
33	8, 32	cfv 6517	. . . . 5 class (Base‘ℎ)
34	33	cpw 4554	. . . 4 class 𝒫 (Base‘ℎ)
35	31, 21, 34	crab 3413	. . 3 class {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})}
36	2, 3, 35	cmpt 5180	. 2 class (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})})
37	1, 36	wceq 1559	1 wff OBasis = (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})})

This definition is referenced by:  isobs  21752