Metamath Proof Explorer

Theorem isobs

Description: The predicate "is an orthonormal basis" (over a pre-Hilbert space). (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypotheses isobs.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
isobs.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
isobs.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
isobs.u ⊢ 1 = ( 1r ‘ 𝐹 )
isobs.z ⊢ 0 = ( 0g ‘ 𝐹 )
isobs.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
isobs.y ⊢ 𝑌 = ( 0g ‘ 𝑊 )
Assertion isobs ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ↔ ( 𝑊 ∈ PreHil ∧ 𝐵 ⊆ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) ) )

Proof

Step Hyp Ref Expression
1 isobs.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 isobs.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 isobs.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 isobs.u ⊢ 1 = ( 1r ‘ 𝐹 )
5 isobs.z ⊢ 0 = ( 0g ‘ 𝐹 )
6 isobs.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
7 isobs.y ⊢ 𝑌 = ( 0g ‘ 𝑊 )
8 df-obs ⊢ OBasis = ( ℎ ∈ PreHil ↦ { 𝑏 ∈ 𝒫 ( Base ‘ ℎ ) ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) ) ∧ ( ( ocv ‘ ℎ ) ‘ 𝑏 ) = { ( 0g ‘ ℎ ) } ) } )
9 8 mptrcl ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → 𝑊 ∈ PreHil )
10 fveq2 ⊢ ( ℎ = 𝑊 → ( Base ‘ ℎ ) = ( Base ‘ 𝑊 ) )
11 10 1 eqtr4di ⊢ ( ℎ = 𝑊 → ( Base ‘ ℎ ) = 𝑉 )
12 11 pweqd ⊢ ( ℎ = 𝑊 → 𝒫 ( Base ‘ ℎ ) = 𝒫 𝑉 )
13 fveq2 ⊢ ( ℎ = 𝑊 → ( ·𝑖 ‘ ℎ ) = ( ·𝑖 ‘ 𝑊 ) )
14 13 2 eqtr4di ⊢ ( ℎ = 𝑊 → ( ·𝑖 ‘ ℎ ) = , )
15 14 oveqd ⊢ ( ℎ = 𝑊 → ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = ( 𝑥 , 𝑦 ) )
16 fveq2 ⊢ ( ℎ = 𝑊 → ( Scalar ‘ ℎ ) = ( Scalar ‘ 𝑊 ) )
17 16 3 eqtr4di ⊢ ( ℎ = 𝑊 → ( Scalar ‘ ℎ ) = 𝐹 )
18 17 fveq2d ⊢ ( ℎ = 𝑊 → ( 1r ‘ ( Scalar ‘ ℎ ) ) = ( 1r ‘ 𝐹 ) )
19 18 4 eqtr4di ⊢ ( ℎ = 𝑊 → ( 1r ‘ ( Scalar ‘ ℎ ) ) = 1 )
20 17 fveq2d ⊢ ( ℎ = 𝑊 → ( 0g ‘ ( Scalar ‘ ℎ ) ) = ( 0g ‘ 𝐹 ) )
21 20 5 eqtr4di ⊢ ( ℎ = 𝑊 → ( 0g ‘ ( Scalar ‘ ℎ ) ) = 0 )
22 19 21 ifeq12d ⊢ ( ℎ = 𝑊 → if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) ) = if ( 𝑥 = 𝑦 , 1 , 0 ) )
23 15 22 eqeq12d ⊢ ( ℎ = 𝑊 → ( ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) ) ↔ ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ) )
24 23 2ralbidv ⊢ ( ℎ = 𝑊 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) ) ↔ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ) )
25 fveq2 ⊢ ( ℎ = 𝑊 → ( ocv ‘ ℎ ) = ( ocv ‘ 𝑊 ) )
26 25 6 eqtr4di ⊢ ( ℎ = 𝑊 → ( ocv ‘ ℎ ) = ⊥ )
27 26 fveq1d ⊢ ( ℎ = 𝑊 → ( ( ocv ‘ ℎ ) ‘ 𝑏 ) = ( ⊥ ‘ 𝑏 ) )
28 fveq2 ⊢ ( ℎ = 𝑊 → ( 0g ‘ ℎ ) = ( 0g ‘ 𝑊 ) )
29 28 7 eqtr4di ⊢ ( ℎ = 𝑊 → ( 0g ‘ ℎ ) = 𝑌 )
30 29 sneqd ⊢ ( ℎ = 𝑊 → { ( 0g ‘ ℎ ) } = { 𝑌 } )
31 27 30 eqeq12d ⊢ ( ℎ = 𝑊 → ( ( ( ocv ‘ ℎ ) ‘ 𝑏 ) = { ( 0g ‘ ℎ ) } ↔ ( ⊥ ‘ 𝑏 ) = { 𝑌 } ) )
32 24 31 anbi12d ⊢ ( ℎ = 𝑊 → ( ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) ) ∧ ( ( ocv ‘ ℎ ) ‘ 𝑏 ) = { ( 0g ‘ ℎ ) } ) ↔ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝑏 ) = { 𝑌 } ) ) )
33 12 32 rabeqbidv ⊢ ( ℎ = 𝑊 → { 𝑏 ∈ 𝒫 ( Base ‘ ℎ ) ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( ·𝑖 ‘ ℎ ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ ℎ ) ) , ( 0g ‘ ( Scalar ‘ ℎ ) ) ) ∧ ( ( ocv ‘ ℎ ) ‘ 𝑏 ) = { ( 0g ‘ ℎ ) } ) } = { 𝑏 ∈ 𝒫 𝑉 ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝑏 ) = { 𝑌 } ) } )
34 1 fvexi ⊢ 𝑉 ∈ V
35 34 pwex ⊢ 𝒫 𝑉 ∈ V
36 35 rabex ⊢ { 𝑏 ∈ 𝒫 𝑉 ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝑏 ) = { 𝑌 } ) } ∈ V
37 33 8 36 fvmpt ⊢ ( 𝑊 ∈ PreHil → ( OBasis ‘ 𝑊 ) = { 𝑏 ∈ 𝒫 𝑉 ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝑏 ) = { 𝑌 } ) } )
38 37 eleq2d ⊢ ( 𝑊 ∈ PreHil → ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ↔ 𝐵 ∈ { 𝑏 ∈ 𝒫 𝑉 ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝑏 ) = { 𝑌 } ) } ) )
39 raleq ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ) )
40 39 raleqbi1dv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ) )
41 fveqeq2 ⊢ ( 𝑏 = 𝐵 → ( ( ⊥ ‘ 𝑏 ) = { 𝑌 } ↔ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) )
42 40 41 anbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝑏 ) = { 𝑌 } ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) ) )
43 42 elrab ⊢ ( 𝐵 ∈ { 𝑏 ∈ 𝒫 𝑉 ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝑏 ) = { 𝑌 } ) } ↔ ( 𝐵 ∈ 𝒫 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) ) )
44 34 elpw2 ⊢ ( 𝐵 ∈ 𝒫 𝑉 ↔ 𝐵 ⊆ 𝑉 )
45 44 anbi1i ⊢ ( ( 𝐵 ∈ 𝒫 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) ) ↔ ( 𝐵 ⊆ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) ) )
46 43 45 bitri ⊢ ( 𝐵 ∈ { 𝑏 ∈ 𝒫 𝑉 ∣ ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝑏 ) = { 𝑌 } ) } ↔ ( 𝐵 ⊆ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) ) )
47 38 46 bitrdi ⊢ ( 𝑊 ∈ PreHil → ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ↔ ( 𝐵 ⊆ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) ) ) )
48 9 47 biadanii ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ↔ ( 𝑊 ∈ PreHil ∧ ( 𝐵 ⊆ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) ) ) )
49 3anass ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ⊆ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) ) ↔ ( 𝑊 ∈ PreHil ∧ ( 𝐵 ⊆ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) ) ) )
50 48 49 bitr4i ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ↔ ( 𝑊 ∈ PreHil ∧ 𝐵 ⊆ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ⊥ ‘ 𝐵 ) = { 𝑌 } ) ) )