Definition df-obs

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)

	Ref	Expression
Assertion	df-obs	⊢ OBasis = ( ℎ ∈ PreHil ↦ { 𝑏 ∈ 𝒫 ( Base ‘ ℎ ) ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) ) ∧ ( ( ocv ‘ ℎ ) ‘ 𝑏 ) = { ( 0g ‘ ℎ ) } ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cobs	⊢ OBasis
1		vh	⊢ ℎ
2		cphl	⊢ PreHil
3		vb	⊢ 𝑏
4		cbs	⊢ Base
5	1	cv	⊢ ℎ
6	5 4	cfv	⊢ ( Base ‘ ℎ )
7	6	cpw	⊢ 𝒫 ( Base ‘ ℎ )
8		vx	⊢ 𝑥
9	3	cv	⊢ 𝑏
10		vy	⊢ 𝑦
11	8	cv	⊢ 𝑥
12		cip	⊢ ·𝑖
13	5 12	cfv	⊢ ( ·𝑖 ‘ ℎ )
14	10	cv	⊢ 𝑦
15	11 14 13	co	⊢ ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 )
16	11 14	wceq	⊢ 𝑥 = 𝑦
17		cur	⊢ 1r
18		csca	⊢ Scalar
19	5 18	cfv	⊢ ( Scalar ‘ ℎ )
20	19 17	cfv	⊢ ( 1r ‘ ( Scalar ‘ ℎ ) )
21		c0g	⊢ 0g
22	19 21	cfv	⊢ ( 0g ‘ ( Scalar ‘ ℎ ) )
23	16 20 22	cif	⊢ if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) )
24	15 23	wceq	⊢ ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) )
25	24 10 9	wral	⊢ ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) )
26	25 8 9	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) )
27		cocv	⊢ ocv
28	5 27	cfv	⊢ ( ocv ‘ ℎ )
29	9 28	cfv	⊢ ( ( ocv ‘ ℎ ) ‘ 𝑏 )
30	5 21	cfv	⊢ ( 0g ‘ ℎ )
31	30	csn	⊢ { ( 0g ‘ ℎ ) }
32	29 31	wceq	⊢ ( ( ocv ‘ ℎ ) ‘ 𝑏 ) = { ( 0g ‘ ℎ ) }
33	26 32	wa	⊢ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) ) ∧ ( ( ocv ‘ ℎ ) ‘ 𝑏 ) = { ( 0g ‘ ℎ ) } )
34	33 3 7	crab	⊢ { 𝑏 ∈ 𝒫 ( Base ‘ ℎ ) ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) ) ∧ ( ( ocv ‘ ℎ ) ‘ 𝑏 ) = { ( 0g ‘ ℎ ) } ) }
35	1 2 34	cmpt	⊢ ( ℎ ∈ PreHil ↦ { 𝑏 ∈ 𝒫 ( Base ‘ ℎ ) ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) ) ∧ ( ( ocv ‘ ℎ ) ‘ 𝑏 ) = { ( 0g ‘ ℎ ) } ) } )
36	0 35	wceq	⊢ OBasis = ( ℎ ∈ PreHil ↦ { 𝑏 ∈ 𝒫 ( Base ‘ ℎ ) ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) ) ∧ ( ( ocv ‘ ℎ ) ‘ 𝑏 ) = { ( 0g ‘ ℎ ) } ) } )