Definition df-obs 22016

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 22013	. 2 class OBasis
2		vh	. . 3 setvar ℎ
3		cphl 21935	. . 3 class PreHil
4		vx	. . . . . . . . . 10 setvar 𝑥
5	4	cv 1568	. . . . . . . . 9 class 𝑥
6		vy	. . . . . . . . . 10 setvar 𝑦
7	6	cv 1568	. . . . . . . . 9 class 𝑦
8	2	cv 1568	. . . . . . . . . 10 class ℎ
9		cip 17438	. . . . . . . . . 10 class ·𝑖
10	8, 9	cfv 6538	. . . . . . . . 9 class (·𝑖‘ℎ)
11	5, 7, 10	co 7420	. . . . . . . 8 class (𝑥(·𝑖‘ℎ)𝑦)
12	4, 6	weq 1994	. . . . . . . . 9 wff 𝑥 = 𝑦
13		csca 17436	. . . . . . . . . . 11 class Scalar
14	8, 13	cfv 6538	. . . . . . . . . 10 class (Scalar‘ℎ)
15		cur 20412	. . . . . . . . . 10 class 1r
16	14, 15	cfv 6538	. . . . . . . . 9 class (1r‘(Scalar‘ℎ))
17		c0g 17615	. . . . . . . . . 10 class 0g
18	14, 17	cfv 6538	. . . . . . . . 9 class (0g‘(Scalar‘ℎ))
19	12, 16, 18	cif 4481	. . . . . . . 8 class if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
20	11, 19	wceq 1569	. . . . . . 7 wff (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
21		vb	. . . . . . . 8 setvar 𝑏
22	21	cv 1568	. . . . . . 7 class 𝑏
23	20, 6, 22	wral 3076	. . . . . 6 wff ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
24	23, 4, 22	wral 3076	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
25		cocv 21971	. . . . . . . 8 class ocv
26	8, 25	cfv 6538	. . . . . . 7 class (ocv‘ℎ)
27	22, 26	cfv 6538	. . . . . 6 class ((ocv‘ℎ)‘𝑏)
28	8, 17	cfv 6538	. . . . . . 7 class (0g‘ℎ)
29	28	csn 4584	. . . . . 6 class {(0g‘ℎ)}
30	27, 29	wceq 1569	. . . . 5 wff ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)}
31	24, 30	wa 401	. . . 4 wff (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})
32		cbs 17392	. . . . . 6 class Base
33	8, 32	cfv 6538	. . . . 5 class (Base‘ℎ)
34	33	cpw 4556	. . . 4 class 𝒫 (Base‘ℎ)
35	31, 21, 34	crab 3412	. . 3 class {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})}
36	2, 3, 35	cmpt 5185	. 2 class (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})})
37	1, 36	wceq 1569	1 wff OBasis = (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})})

This definition is used by:  isobs  22031