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 ) ) ) ) |