Metamath Proof Explorer

Theorem isphl

Description: The predicate "is a generalized pre-Hilbert (inner product) space". (Contributed by NM, 22-Sep-2011) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses isphl.v 
|- V = ( Base ` W )
isphl.f 
|- F = ( Scalar ` W )
isphl.h 
|- ., = ( .i ` W )
isphl.o 
|- .0. = ( 0g ` W )
isphl.i 
|- .* = ( *r ` F )
isphl.z 
|- Z = ( 0g ` F )
Assertion isphl 
|- ( W e. PreHil <-> ( W e. LVec /\ F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) )

Proof

Step Hyp Ref Expression
1 isphl.v 
 |-  V = ( Base ` W )
2 isphl.f 
 |-  F = ( Scalar ` W )
3 isphl.h 
 |-  ., = ( .i ` W )
4 isphl.o 
 |-  .0. = ( 0g ` W )
5 isphl.i 
 |-  .* = ( *r ` F )
6 isphl.z 
 |-  Z = ( 0g ` F )
7 fvexd 
 |-  ( g = W -> ( Base ` g ) e. _V )
8 fvexd 
 |-  ( ( g = W /\ v = ( Base ` g ) ) -> ( .i ` g ) e. _V )
9 fvexd 
 |-  ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> ( Scalar ` g ) e. _V )
10 id 
 |-  ( f = ( Scalar ` g ) -> f = ( Scalar ` g ) )
11 simpll 
 |-  ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> g = W )
12 11 fveq2d 
 |-  ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> ( Scalar ` g ) = ( Scalar ` W ) )
13 12 2 eqtr4di 
 |-  ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> ( Scalar ` g ) = F )
14 10 13 sylan9eqr 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> f = F )
15 14 eleq1d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( f e. *Ring <-> F e. *Ring ) )
16 simpllr 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> v = ( Base ` g ) )
17 simplll 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> g = W )
18 17 fveq2d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( Base ` g ) = ( Base ` W ) )
19 18 1 eqtr4di 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( Base ` g ) = V )
20 16 19 eqtrd 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> v = V )
21 simplr 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> h = ( .i ` g ) )
22 17 fveq2d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( .i ` g ) = ( .i ` W ) )
23 22 3 eqtr4di 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( .i ` g ) = ., )
24 21 23 eqtrd 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> h = ., )
25 24 oveqd 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( y h x ) = ( y ., x ) )
26 20 25 mpteq12dv 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( y e. v |-> ( y h x ) ) = ( y e. V |-> ( y ., x ) ) )
27 14 fveq2d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( ringLMod ` f ) = ( ringLMod ` F ) )
28 17 27 oveq12d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( g LMHom ( ringLMod ` f ) ) = ( W LMHom ( ringLMod ` F ) ) )
29 26 28 eleq12d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( ( y e. v |-> ( y h x ) ) e. ( g LMHom ( ringLMod ` f ) ) <-> ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) ) )
30 24 oveqd 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( x h x ) = ( x ., x ) )
31 14 fveq2d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( 0g ` f ) = ( 0g ` F ) )
32 31 6 eqtr4di 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( 0g ` f ) = Z )
33 30 32 eqeq12d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( ( x h x ) = ( 0g ` f ) <-> ( x ., x ) = Z ) )
34 17 fveq2d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( 0g ` g ) = ( 0g ` W ) )
35 34 4 eqtr4di 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( 0g ` g ) = .0. )
36 35 eqeq2d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( x = ( 0g ` g ) <-> x = .0. ) )
37 33 36 imbi12d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) <-> ( ( x ., x ) = Z -> x = .0. ) ) )
38 14 fveq2d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( *r ` f ) = ( *r ` F ) )
39 38 5 eqtr4di 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( *r ` f ) = .* )
40 24 oveqd 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( x h y ) = ( x ., y ) )
41 39 40 fveq12d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( ( *r ` f ) ` ( x h y ) ) = ( .* ` ( x ., y ) ) )
42 41 25 eqeq12d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) <-> ( .* ` ( x ., y ) ) = ( y ., x ) ) )
43 20 42 raleqbidv 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) <-> A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) )
44 29 37 43 3anbi123d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( ( ( y e. v |-> ( y h x ) ) e. ( g LMHom ( ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) <-> ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) )
45 20 44 raleqbidv 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom ( ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) <-> A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) )
46 15 45 anbi12d 
 |-  ( ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) /\ f = ( Scalar ` g ) ) -> ( ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom ( ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) <-> ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
47 9 46 sbcied 
 |-  ( ( ( g = W /\ v = ( Base ` g ) ) /\ h = ( .i ` g ) ) -> ( [. ( Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom ( ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) <-> ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
48 8 47 sbcied 
 |-  ( ( g = W /\ v = ( Base ` g ) ) -> ( [. ( .i ` g ) / h ]. [. ( Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom ( ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) <-> ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
49 7 48 sbcied 
 |-  ( g = W -> ( [. ( Base ` g ) / v ]. [. ( .i ` g ) / h ]. [. ( Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom ( ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) <-> ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
50 df-phl 
 |-  PreHil = { g e. LVec | [. ( Base ` g ) / v ]. [. ( .i ` g ) / h ]. [. ( Scalar ` g ) / f ]. ( f e. *Ring /\ A. x e. v ( ( y e. v |-> ( y h x ) ) e. ( g LMHom ( ringLMod ` f ) ) /\ ( ( x h x ) = ( 0g ` f ) -> x = ( 0g ` g ) ) /\ A. y e. v ( ( *r ` f ) ` ( x h y ) ) = ( y h x ) ) ) }
51 49 50 elrab2 
 |-  ( W e. PreHil <-> ( W e. LVec /\ ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
52 3anass 
 |-  ( ( W e. LVec /\ F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) <-> ( W e. LVec /\ ( F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) ) )
53 51 52 bitr4i 
 |-  ( W e. PreHil <-> ( W e. LVec /\ F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = Z -> x = .0. ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) )