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 
|- V = ( Base ` W )
isobs.h 
|- ., = ( .i ` W )
isobs.f 
|- F = ( Scalar ` W )
isobs.u 
|- .1. = ( 1r ` F )
isobs.z 
|- .0. = ( 0g ` F )
Assertion obsip 
|- ( ( B e. ( OBasis ` W ) /\ P e. B /\ Q e. B ) -> ( P ., Q ) = if ( P = Q , .1. , .0. ) )

Proof

Step Hyp Ref Expression
1 isobs.v 
 |-  V = ( Base ` W )
2 isobs.h 
 |-  ., = ( .i ` W )
3 isobs.f 
 |-  F = ( Scalar ` W )
4 isobs.u 
 |-  .1. = ( 1r ` F )
5 isobs.z 
 |-  .0. = ( 0g ` F )
6 eqid 
 |-  ( ocv ` W ) = ( ocv ` W )
7 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
8 1 2 3 4 5 6 7 isobs 
 |-  ( B e. ( OBasis ` W ) <-> ( W e. PreHil /\ B C_ V /\ ( A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ( ocv ` W ) ` B ) = { ( 0g ` W ) } ) ) )
9 8 simp3bi 
 |-  ( B e. ( OBasis ` W ) -> ( A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ( ocv ` W ) ` B ) = { ( 0g ` W ) } ) )
10 9 simpld 
 |-  ( B e. ( OBasis ` W ) -> A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) )
11 oveq1 
 |-  ( x = P -> ( x ., y ) = ( P ., y ) )
12 eqeq1 
 |-  ( x = P -> ( x = y <-> P = y ) )
13 12 ifbid 
 |-  ( x = P -> if ( x = y , .1. , .0. ) = if ( P = y , .1. , .0. ) )
14 11 13 eqeq12d 
 |-  ( x = P -> ( ( x ., y ) = if ( x = y , .1. , .0. ) <-> ( P ., y ) = if ( P = y , .1. , .0. ) ) )
15 oveq2 
 |-  ( y = Q -> ( P ., y ) = ( P ., Q ) )
16 eqeq2 
 |-  ( y = Q -> ( P = y <-> P = Q ) )
17 16 ifbid 
 |-  ( y = Q -> if ( P = y , .1. , .0. ) = if ( P = Q , .1. , .0. ) )
18 15 17 eqeq12d 
 |-  ( y = Q -> ( ( P ., y ) = if ( P = y , .1. , .0. ) <-> ( P ., Q ) = if ( P = Q , .1. , .0. ) ) )
19 14 18 rspc2v 
 |-  ( ( P e. B /\ Q e. B ) -> ( A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) -> ( P ., Q ) = if ( P = Q , .1. , .0. ) ) )
20 10 19 syl5com 
 |-  ( B e. ( OBasis ` W ) -> ( ( P e. B /\ Q e. B ) -> ( P ., Q ) = if ( P = Q , .1. , .0. ) ) )
21 20 3impib 
 |-  ( ( B e. ( OBasis ` W ) /\ P e. B /\ Q e. B ) -> ( P ., Q ) = if ( P = Q , .1. , .0. ) )