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