Definition df-obs 22041

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 22038	. 2 class OBasis
2		vh	. . 3 setvar ℎ
3		cphl 21960	. . 3 class PreHil
4		vx	. . . . . . . . . 10 setvar 𝑥
5	4	cv 1569	. . . . . . . . 9 class 𝑥
6		vy	. . . . . . . . . 10 setvar 𝑦
7	6	cv 1569	. . . . . . . . 9 class 𝑦
8	2	cv 1569	. . . . . . . . . 10 class ℎ
9		cip 17462	. . . . . . . . . 10 class ·𝑖
10	8, 9	cfv 6558	. . . . . . . . 9 class (·𝑖‘ℎ)
11	5, 7, 10	co 7443	. . . . . . . 8 class (𝑥(·𝑖‘ℎ)𝑦)
12	4, 6	weq 1997	. . . . . . . . 9 wff 𝑥 = 𝑦
13		csca 17460	. . . . . . . . . . 11 class Scalar
14	8, 13	cfv 6558	. . . . . . . . . 10 class (Scalar‘ℎ)
15		cur 20437	. . . . . . . . . 10 class 1r
16	14, 15	cfv 6558	. . . . . . . . 9 class (1r‘(Scalar‘ℎ))
17		c0g 17639	. . . . . . . . . 10 class 0g
18	14, 17	cfv 6558	. . . . . . . . 9 class (0g‘(Scalar‘ℎ))
19	12, 16, 18	cif 4485	. . . . . . . 8 class if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
20	11, 19	wceq 1570	. . . . . . 7 wff (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
21		vb	. . . . . . . 8 setvar 𝑏
22	21	cv 1569	. . . . . . 7 class 𝑏
23	20, 6, 22	wral 3080	. . . . . 6 wff ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
24	23, 4, 22	wral 3080	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ)))
25		cocv 21996	. . . . . . . 8 class ocv
26	8, 25	cfv 6558	. . . . . . 7 class (ocv‘ℎ)
27	22, 26	cfv 6558	. . . . . 6 class ((ocv‘ℎ)‘𝑏)
28	8, 17	cfv 6558	. . . . . . 7 class (0g‘ℎ)
29	28	csn 4588	. . . . . 6 class {(0g‘ℎ)}
30	27, 29	wceq 1570	. . . . 5 wff ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)}
31	24, 30	wa 401	. . . 4 wff (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})
32		cbs 17416	. . . . . 6 class Base
33	8, 32	cfv 6558	. . . . 5 class (Base‘ℎ)
34	33	cpw 4560	. . . 4 class 𝒫 (Base‘ℎ)
35	31, 21, 34	crab 3416	. . 3 class {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})}
36	2, 3, 35	cmpt 5189	. 2 class (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})})
37	1, 36	wceq 1570	1 wff OBasis = (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)), (0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})})

This definition is used by:  isobs  22056