Metamath Proof Explorer

Theorem lcf1o

Description: Define a function J that provides a bijection from nonzero vectors V to nonzero functionals with closed kernels C . (Contributed by NM, 22-Feb-2015)

Ref Expression
Hypotheses lcf1o.h 
|- H = ( LHyp ` K )
lcf1o.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcf1o.u 
|- U = ( ( DVecH ` K ) ` W )
lcf1o.v 
|- V = ( Base ` U )
lcf1o.a 
|- .+ = ( +g ` U )
lcf1o.t 
|- .x. = ( .s ` U )
lcf1o.s 
|- S = ( Scalar ` U )
lcf1o.r 
|- R = ( Base ` S )
lcf1o.z 
|- .0. = ( 0g ` U )
lcf1o.f 
|- F = ( LFnl ` U )
lcf1o.l 
|- L = ( LKer ` U )
lcf1o.d 
|- D = ( LDual ` U )
lcf1o.q 
|- Q = ( 0g ` D )
lcf1o.c 
|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
lcf1o.j 
|- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
lcflo.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion lcf1o 
|- ( ph -> J : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) )

Proof

Step Hyp Ref Expression
1 lcf1o.h 
 |-  H = ( LHyp ` K )
2 lcf1o.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcf1o.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcf1o.v 
 |-  V = ( Base ` U )
5 lcf1o.a 
 |-  .+ = ( +g ` U )
6 lcf1o.t 
 |-  .x. = ( .s ` U )
7 lcf1o.s 
 |-  S = ( Scalar ` U )
8 lcf1o.r 
 |-  R = ( Base ` S )
9 lcf1o.z 
 |-  .0. = ( 0g ` U )
10 lcf1o.f 
 |-  F = ( LFnl ` U )
11 lcf1o.l 
 |-  L = ( LKer ` U )
12 lcf1o.d 
 |-  D = ( LDual ` U )
13 lcf1o.q 
 |-  Q = ( 0g ` D )
14 lcf1o.c 
 |-  C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
15 lcf1o.j 
 |-  J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
16 lcflo.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
17 oveq1 
 |-  ( w = z -> ( w .+ ( k .x. x ) ) = ( z .+ ( k .x. x ) ) )
18 17 eqeq2d 
 |-  ( w = z -> ( v = ( w .+ ( k .x. x ) ) <-> v = ( z .+ ( k .x. x ) ) ) )
19 18 cbvrexvw 
 |-  ( E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) <-> E. z e. ( ._|_ ` { x } ) v = ( z .+ ( k .x. x ) ) )
20 oveq1 
 |-  ( k = l -> ( k .x. x ) = ( l .x. x ) )
21 20 oveq2d 
 |-  ( k = l -> ( z .+ ( k .x. x ) ) = ( z .+ ( l .x. x ) ) )
22 21 eqeq2d 
 |-  ( k = l -> ( v = ( z .+ ( k .x. x ) ) <-> v = ( z .+ ( l .x. x ) ) ) )
23 22 rexbidv 
 |-  ( k = l -> ( E. z e. ( ._|_ ` { x } ) v = ( z .+ ( k .x. x ) ) <-> E. z e. ( ._|_ ` { x } ) v = ( z .+ ( l .x. x ) ) ) )
24 19 23 syl5bb 
 |-  ( k = l -> ( E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) <-> E. z e. ( ._|_ ` { x } ) v = ( z .+ ( l .x. x ) ) ) )
25 24 cbvriotavw 
 |-  ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) = ( iota_ l e. R E. z e. ( ._|_ ` { x } ) v = ( z .+ ( l .x. x ) ) )
26 eqeq1 
 |-  ( v = u -> ( v = ( z .+ ( l .x. x ) ) <-> u = ( z .+ ( l .x. x ) ) ) )
27 26 rexbidv 
 |-  ( v = u -> ( E. z e. ( ._|_ ` { x } ) v = ( z .+ ( l .x. x ) ) <-> E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) )
28 27 riotabidv 
 |-  ( v = u -> ( iota_ l e. R E. z e. ( ._|_ ` { x } ) v = ( z .+ ( l .x. x ) ) ) = ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) )
29 25 28 syl5eq 
 |-  ( v = u -> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) = ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) )
30 29 cbvmptv 
 |-  ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) )
31 sneq 
 |-  ( x = y -> { x } = { y } )
32 31 fveq2d 
 |-  ( x = y -> ( ._|_ ` { x } ) = ( ._|_ ` { y } ) )
33 oveq2 
 |-  ( x = y -> ( l .x. x ) = ( l .x. y ) )
34 33 oveq2d 
 |-  ( x = y -> ( z .+ ( l .x. x ) ) = ( z .+ ( l .x. y ) ) )
35 34 eqeq2d 
 |-  ( x = y -> ( u = ( z .+ ( l .x. x ) ) <-> u = ( z .+ ( l .x. y ) ) ) )
36 32 35 rexeqbidv 
 |-  ( x = y -> ( E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) <-> E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) )
37 36 riotabidv 
 |-  ( x = y -> ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) = ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) )
38 37 mpteq2dv 
 |-  ( x = y -> ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) ) = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) )
39 30 38 syl5eq 
 |-  ( x = y -> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) )
40 39 cbvmptv 
 |-  ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) = ( y e. ( V \ { .0. } ) |-> ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) )
41 15 40 eqtri 
 |-  J = ( y e. ( V \ { .0. } ) |-> ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) )
42 1 2 3 4 5 6 7 8 9 10 11 12 13 14 41 16 lcfrlem9 
 |-  ( ph -> J : ( V \ { .0. } ) -1-1-onto-> ( C \ { Q } ) )