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 
|- V = ( Base ` W )
isobs.h 
|- ., = ( .i ` W )
isobs.f 
|- F = ( Scalar ` W )
isobs.u 
|- .1. = ( 1r ` F )
isobs.z 
|- .0. = ( 0g ` F )
isobs.o 
|- ._|_ = ( ocv ` W )
isobs.y 
|- Y = ( 0g ` W )
Assertion 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. ) /\ ( ._|_ ` B ) = { Y } ) ) )

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 isobs.o 
 |-  ._|_ = ( ocv ` W )
7 isobs.y 
 |-  Y = ( 0g ` W )
8 df-obs 
 |-  OBasis = ( h e. PreHil |-> { b e. ~P ( Base ` h ) | ( A. x e. b A. y e. b ( x ( .i ` h ) y ) = if ( x = y , ( 1r ` ( Scalar ` h ) ) , ( 0g ` ( Scalar ` h ) ) ) /\ ( ( ocv ` h ) ` b ) = { ( 0g ` h ) } ) } )
9 8 mptrcl 
 |-  ( B e. ( OBasis ` W ) -> W e. PreHil )
10 fveq2 
 |-  ( h = W -> ( Base ` h ) = ( Base ` W ) )
11 10 1 eqtr4di 
 |-  ( h = W -> ( Base ` h ) = V )
12 11 pweqd 
 |-  ( h = W -> ~P ( Base ` h ) = ~P V )
13 fveq2 
 |-  ( h = W -> ( .i ` h ) = ( .i ` W ) )
14 13 2 eqtr4di 
 |-  ( h = W -> ( .i ` h ) = ., )
15 14 oveqd 
 |-  ( h = W -> ( x ( .i ` h ) y ) = ( x ., y ) )
16 fveq2 
 |-  ( h = W -> ( Scalar ` h ) = ( Scalar ` W ) )
17 16 3 eqtr4di 
 |-  ( h = W -> ( Scalar ` h ) = F )
18 17 fveq2d 
 |-  ( h = W -> ( 1r ` ( Scalar ` h ) ) = ( 1r ` F ) )
19 18 4 eqtr4di 
 |-  ( h = W -> ( 1r ` ( Scalar ` h ) ) = .1. )
20 17 fveq2d 
 |-  ( h = W -> ( 0g ` ( Scalar ` h ) ) = ( 0g ` F ) )
21 20 5 eqtr4di 
 |-  ( h = W -> ( 0g ` ( Scalar ` h ) ) = .0. )
22 19 21 ifeq12d 
 |-  ( h = W -> if ( x = y , ( 1r ` ( Scalar ` h ) ) , ( 0g ` ( Scalar ` h ) ) ) = if ( x = y , .1. , .0. ) )
23 15 22 eqeq12d 
 |-  ( h = W -> ( ( x ( .i ` h ) y ) = if ( x = y , ( 1r ` ( Scalar ` h ) ) , ( 0g ` ( Scalar ` h ) ) ) <-> ( x ., y ) = if ( x = y , .1. , .0. ) ) )
24 23 2ralbidv 
 |-  ( h = W -> ( A. x e. b A. y e. b ( x ( .i ` h ) y ) = if ( x = y , ( 1r ` ( Scalar ` h ) ) , ( 0g ` ( Scalar ` h ) ) ) <-> A. x e. b A. y e. b ( x ., y ) = if ( x = y , .1. , .0. ) ) )
25 fveq2 
 |-  ( h = W -> ( ocv ` h ) = ( ocv ` W ) )
26 25 6 eqtr4di 
 |-  ( h = W -> ( ocv ` h ) = ._|_ )
27 26 fveq1d 
 |-  ( h = W -> ( ( ocv ` h ) ` b ) = ( ._|_ ` b ) )
28 fveq2 
 |-  ( h = W -> ( 0g ` h ) = ( 0g ` W ) )
29 28 7 eqtr4di 
 |-  ( h = W -> ( 0g ` h ) = Y )
30 29 sneqd 
 |-  ( h = W -> { ( 0g ` h ) } = { Y } )
31 27 30 eqeq12d 
 |-  ( h = W -> ( ( ( ocv ` h ) ` b ) = { ( 0g ` h ) } <-> ( ._|_ ` b ) = { Y } ) )
32 24 31 anbi12d 
 |-  ( h = W -> ( ( A. x e. b A. y e. b ( x ( .i ` h ) y ) = if ( x = y , ( 1r ` ( Scalar ` h ) ) , ( 0g ` ( Scalar ` h ) ) ) /\ ( ( ocv ` h ) ` b ) = { ( 0g ` h ) } ) <-> ( A. x e. b A. y e. b ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` b ) = { Y } ) ) )
33 12 32 rabeqbidv 
 |-  ( h = W -> { b e. ~P ( Base ` h ) | ( A. x e. b A. y e. b ( x ( .i ` h ) y ) = if ( x = y , ( 1r ` ( Scalar ` h ) ) , ( 0g ` ( Scalar ` h ) ) ) /\ ( ( ocv ` h ) ` b ) = { ( 0g ` h ) } ) } = { b e. ~P V | ( A. x e. b A. y e. b ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` b ) = { Y } ) } )
34 1 fvexi 
 |-  V e. _V
35 34 pwex 
 |-  ~P V e. _V
36 35 rabex 
 |-  { b e. ~P V | ( A. x e. b A. y e. b ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` b ) = { Y } ) } e. _V
37 33 8 36 fvmpt 
 |-  ( W e. PreHil -> ( OBasis ` W ) = { b e. ~P V | ( A. x e. b A. y e. b ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` b ) = { Y } ) } )
38 37 eleq2d 
 |-  ( W e. PreHil -> ( B e. ( OBasis ` W ) <-> B e. { b e. ~P V | ( A. x e. b A. y e. b ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` b ) = { Y } ) } ) )
39 raleq 
 |-  ( b = B -> ( A. y e. b ( x ., y ) = if ( x = y , .1. , .0. ) <-> A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) ) )
40 39 raleqbi1dv 
 |-  ( b = B -> ( A. x e. b A. y e. b ( x ., y ) = if ( x = y , .1. , .0. ) <-> A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) ) )
41 fveqeq2 
 |-  ( b = B -> ( ( ._|_ ` b ) = { Y } <-> ( ._|_ ` B ) = { Y } ) )
42 40 41 anbi12d 
 |-  ( b = B -> ( ( A. x e. b A. y e. b ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` b ) = { Y } ) <-> ( A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` B ) = { Y } ) ) )
43 42 elrab 
 |-  ( B e. { b e. ~P V | ( A. x e. b A. y e. b ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` b ) = { Y } ) } <-> ( B e. ~P V /\ ( A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` B ) = { Y } ) ) )
44 34 elpw2 
 |-  ( B e. ~P V <-> B C_ V )
45 44 anbi1i 
 |-  ( ( B e. ~P V /\ ( A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` B ) = { Y } ) ) <-> ( B C_ V /\ ( A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` B ) = { Y } ) ) )
46 43 45 bitri 
 |-  ( B e. { b e. ~P V | ( A. x e. b A. y e. b ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` b ) = { Y } ) } <-> ( B C_ V /\ ( A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` B ) = { Y } ) ) )
47 38 46 bitrdi 
 |-  ( W e. PreHil -> ( B e. ( OBasis ` W ) <-> ( B C_ V /\ ( A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` B ) = { Y } ) ) ) )
48 9 47 biadanii 
 |-  ( 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. ) /\ ( ._|_ ` B ) = { Y } ) ) ) )
49 3anass 
 |-  ( ( W e. PreHil /\ B C_ V /\ ( A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` B ) = { Y } ) ) <-> ( W e. PreHil /\ ( B C_ V /\ ( A. x e. B A. y e. B ( x ., y ) = if ( x = y , .1. , .0. ) /\ ( ._|_ ` B ) = { Y } ) ) ) )
50 48 49 bitr4i 
 |-  ( 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. ) /\ ( ._|_ ` B ) = { Y } ) ) )