Metamath Proof Explorer


Theorem lcfl7N

Description: Property of a functional with a closed kernel. Every nonzero functional is determined by a unique nonzero vector. Note that ( LG ) = V means the functional is zero by lkr0f . (Contributed by NM, 4-Jan-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lcfl6.h
|- H = ( LHyp ` K )
lcfl6.o
|- ._|_ = ( ( ocH ` K ) ` W )
lcfl6.u
|- U = ( ( DVecH ` K ) ` W )
lcfl6.v
|- V = ( Base ` U )
lcfl6.a
|- .+ = ( +g ` U )
lcfl6.t
|- .x. = ( .s ` U )
lcfl6.s
|- S = ( Scalar ` U )
lcfl6.r
|- R = ( Base ` S )
lcfl6.z
|- .0. = ( 0g ` U )
lcfl6.f
|- F = ( LFnl ` U )
lcfl6.l
|- L = ( LKer ` U )
lcfl6.c
|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
lcfl6.k
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfl6.g
|- ( ph -> G e. F )
Assertion lcfl7N
|- ( ph -> ( G e. C <-> ( ( L ` G ) = V \/ E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lcfl6.h
 |-  H = ( LHyp ` K )
2 lcfl6.o
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfl6.u
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfl6.v
 |-  V = ( Base ` U )
5 lcfl6.a
 |-  .+ = ( +g ` U )
6 lcfl6.t
 |-  .x. = ( .s ` U )
7 lcfl6.s
 |-  S = ( Scalar ` U )
8 lcfl6.r
 |-  R = ( Base ` S )
9 lcfl6.z
 |-  .0. = ( 0g ` U )
10 lcfl6.f
 |-  F = ( LFnl ` U )
11 lcfl6.l
 |-  L = ( LKer ` U )
12 lcfl6.c
 |-  C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
13 lcfl6.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
14 lcfl6.g
 |-  ( ph -> G e. F )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 lcfl6
 |-  ( ph -> ( G e. C <-> ( ( L ` G ) = V \/ E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) )
16 13 ad2antrr
 |-  ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> ( K e. HL /\ W e. H ) )
17 eqid
 |-  ( 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. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) )
18 eqid
 |-  ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) )
19 simplrl
 |-  ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> x e. ( V \ { .0. } ) )
20 simplrr
 |-  ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> y e. ( V \ { .0. } ) )
21 simprl
 |-  ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
22 eqeq1
 |-  ( v = u -> ( v = ( w .+ ( k .x. x ) ) <-> u = ( w .+ ( k .x. x ) ) ) )
23 22 rexbidv
 |-  ( v = u -> ( E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) <-> E. w e. ( ._|_ ` { x } ) u = ( w .+ ( k .x. x ) ) ) )
24 23 riotabidv
 |-  ( v = u -> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) = ( iota_ k e. R E. w e. ( ._|_ ` { x } ) u = ( w .+ ( k .x. x ) ) ) )
25 oveq1
 |-  ( k = l -> ( k .x. x ) = ( l .x. x ) )
26 25 oveq2d
 |-  ( k = l -> ( w .+ ( k .x. x ) ) = ( w .+ ( l .x. x ) ) )
27 26 eqeq2d
 |-  ( k = l -> ( u = ( w .+ ( k .x. x ) ) <-> u = ( w .+ ( l .x. x ) ) ) )
28 27 rexbidv
 |-  ( k = l -> ( E. w e. ( ._|_ ` { x } ) u = ( w .+ ( k .x. x ) ) <-> E. w e. ( ._|_ ` { x } ) u = ( w .+ ( l .x. x ) ) ) )
29 oveq1
 |-  ( w = z -> ( w .+ ( l .x. x ) ) = ( z .+ ( l .x. x ) ) )
30 29 eqeq2d
 |-  ( w = z -> ( u = ( w .+ ( l .x. x ) ) <-> u = ( z .+ ( l .x. x ) ) ) )
31 30 cbvrexvw
 |-  ( E. w e. ( ._|_ ` { x } ) u = ( w .+ ( l .x. x ) ) <-> E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) )
32 28 31 bitrdi
 |-  ( k = l -> ( E. w e. ( ._|_ ` { x } ) u = ( w .+ ( k .x. x ) ) <-> E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) )
33 32 cbvriotavw
 |-  ( iota_ k e. R E. w e. ( ._|_ ` { x } ) u = ( w .+ ( k .x. x ) ) ) = ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) )
34 24 33 eqtrdi
 |-  ( 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 ) ) ) )
35 34 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 ) ) ) )
36 21 35 eqtrdi
 |-  ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> G = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { x } ) u = ( z .+ ( l .x. x ) ) ) ) )
37 simprr
 |-  ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) )
38 eqeq1
 |-  ( v = u -> ( v = ( w .+ ( k .x. y ) ) <-> u = ( w .+ ( k .x. y ) ) ) )
39 38 rexbidv
 |-  ( v = u -> ( E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) <-> E. w e. ( ._|_ ` { y } ) u = ( w .+ ( k .x. y ) ) ) )
40 39 riotabidv
 |-  ( v = u -> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) = ( iota_ k e. R E. w e. ( ._|_ ` { y } ) u = ( w .+ ( k .x. y ) ) ) )
41 oveq1
 |-  ( k = l -> ( k .x. y ) = ( l .x. y ) )
42 41 oveq2d
 |-  ( k = l -> ( w .+ ( k .x. y ) ) = ( w .+ ( l .x. y ) ) )
43 42 eqeq2d
 |-  ( k = l -> ( u = ( w .+ ( k .x. y ) ) <-> u = ( w .+ ( l .x. y ) ) ) )
44 43 rexbidv
 |-  ( k = l -> ( E. w e. ( ._|_ ` { y } ) u = ( w .+ ( k .x. y ) ) <-> E. w e. ( ._|_ ` { y } ) u = ( w .+ ( l .x. y ) ) ) )
45 oveq1
 |-  ( w = z -> ( w .+ ( l .x. y ) ) = ( z .+ ( l .x. y ) ) )
46 45 eqeq2d
 |-  ( w = z -> ( u = ( w .+ ( l .x. y ) ) <-> u = ( z .+ ( l .x. y ) ) ) )
47 46 cbvrexvw
 |-  ( E. w e. ( ._|_ ` { y } ) u = ( w .+ ( l .x. y ) ) <-> E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) )
48 44 47 bitrdi
 |-  ( k = l -> ( E. w e. ( ._|_ ` { y } ) u = ( w .+ ( k .x. y ) ) <-> E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) )
49 48 cbvriotavw
 |-  ( iota_ k e. R E. w e. ( ._|_ ` { y } ) u = ( w .+ ( k .x. y ) ) ) = ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) )
50 40 49 eqtrdi
 |-  ( v = u -> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) = ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) )
51 50 cbvmptv
 |-  ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) )
52 37 51 eqtrdi
 |-  ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> G = ( u e. V |-> ( iota_ l e. R E. z e. ( ._|_ ` { y } ) u = ( z .+ ( l .x. y ) ) ) ) )
53 36 52 eqtr3d
 |-  ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .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 ) ) ) ) )
54 1 2 3 4 5 6 7 8 9 10 11 16 17 18 19 20 53 lcfl7lem
 |-  ( ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) /\ ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) ) -> x = y )
55 54 ex
 |-  ( ( ph /\ ( x e. ( V \ { .0. } ) /\ y e. ( V \ { .0. } ) ) ) -> ( ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) -> x = y ) )
56 55 ralrimivva
 |-  ( ph -> A. x e. ( V \ { .0. } ) A. y e. ( V \ { .0. } ) ( ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) -> x = y ) )
57 56 a1d
 |-  ( ph -> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) -> A. x e. ( V \ { .0. } ) A. y e. ( V \ { .0. } ) ( ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) -> x = y ) ) )
58 57 ancld
 |-  ( ph -> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) -> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ A. x e. ( V \ { .0. } ) A. y e. ( V \ { .0. } ) ( ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) -> x = y ) ) ) )
59 sneq
 |-  ( x = y -> { x } = { y } )
60 59 fveq2d
 |-  ( x = y -> ( ._|_ ` { x } ) = ( ._|_ ` { y } ) )
61 oveq2
 |-  ( x = y -> ( k .x. x ) = ( k .x. y ) )
62 61 oveq2d
 |-  ( x = y -> ( w .+ ( k .x. x ) ) = ( w .+ ( k .x. y ) ) )
63 62 eqeq2d
 |-  ( x = y -> ( v = ( w .+ ( k .x. x ) ) <-> v = ( w .+ ( k .x. y ) ) ) )
64 60 63 rexeqbidv
 |-  ( x = y -> ( E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) <-> E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) )
65 64 riotabidv
 |-  ( x = y -> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) = ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) )
66 65 mpteq2dv
 |-  ( x = y -> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) )
67 66 eqeq2d
 |-  ( x = y -> ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) <-> G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) )
68 67 reu4
 |-  ( E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) <-> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ A. x e. ( V \ { .0. } ) A. y e. ( V \ { .0. } ) ( ( G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { y } ) v = ( w .+ ( k .x. y ) ) ) ) ) -> x = y ) ) )
69 58 68 syl6ibr
 |-  ( ph -> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) -> E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) )
70 reurex
 |-  ( E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) -> E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
71 69 70 impbid1
 |-  ( ph -> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) <-> E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) )
72 71 orbi2d
 |-  ( ph -> ( ( ( L ` G ) = V \/ E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) <-> ( ( L ` G ) = V \/ E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) )
73 15 72 bitrd
 |-  ( ph -> ( G e. C <-> ( ( L ` G ) = V \/ E! x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) ) )