Metamath Proof Explorer

Theorem obsip

Description: The inner product of two elements of an orthonormal basis. (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 ‘ 𝐹 )
Assertion obsip ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 , 𝑄 ) = 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 eqid ⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
7 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
8 1 2 3 4 5 6 7 isobs ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ↔ ( 𝑊 ∈ PreHil ∧ 𝐵 ⊆ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ( ocv ‘ 𝑊 ) ‘ 𝐵 ) = { ( 0g ‘ 𝑊 ) } ) ) )
9 8 simp3bi ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ∧ ( ( ocv ‘ 𝑊 ) ‘ 𝐵 ) = { ( 0g ‘ 𝑊 ) } ) )
10 9 simpld ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) )
11 oveq1 ⊢ ( 𝑥 = 𝑃 → ( 𝑥 , 𝑦 ) = ( 𝑃 , 𝑦 ) )
12 eqeq1 ⊢ ( 𝑥 = 𝑃 → ( 𝑥 = 𝑦 ↔ 𝑃 = 𝑦 ) )
13 12 ifbid ⊢ ( 𝑥 = 𝑃 → if ( 𝑥 = 𝑦 , 1 , 0 ) = if ( 𝑃 = 𝑦 , 1 , 0 ) )
14 11 13 eqeq12d ⊢ ( 𝑥 = 𝑃 → ( ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) ↔ ( 𝑃 , 𝑦 ) = if ( 𝑃 = 𝑦 , 1 , 0 ) ) )
15 oveq2 ⊢ ( 𝑦 = 𝑄 → ( 𝑃 , 𝑦 ) = ( 𝑃 , 𝑄 ) )
16 eqeq2 ⊢ ( 𝑦 = 𝑄 → ( 𝑃 = 𝑦 ↔ 𝑃 = 𝑄 ) )
17 16 ifbid ⊢ ( 𝑦 = 𝑄 → if ( 𝑃 = 𝑦 , 1 , 0 ) = if ( 𝑃 = 𝑄 , 1 , 0 ) )
18 15 17 eqeq12d ⊢ ( 𝑦 = 𝑄 → ( ( 𝑃 , 𝑦 ) = if ( 𝑃 = 𝑦 , 1 , 0 ) ↔ ( 𝑃 , 𝑄 ) = if ( 𝑃 = 𝑄 , 1 , 0 ) ) )
19 14 18 rspc2v ⊢ ( ( 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 , 𝑦 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) → ( 𝑃 , 𝑄 ) = if ( 𝑃 = 𝑄 , 1 , 0 ) ) )
20 10 19 syl5com ⊢ ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → ( ( 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 , 𝑄 ) = if ( 𝑃 = 𝑄 , 1 , 0 ) ) )
21 20 3impib ⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 , 𝑄 ) = if ( 𝑃 = 𝑄 , 1 , 0 ) )