Metamath Proof Explorer

Theorem lcfl8b

Description: Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015)

Ref Expression
Hypotheses lcfl8b.h 
|- H = ( LHyp ` K )
lcfl8b.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcfl8b.u 
|- U = ( ( DVecH ` K ) ` W )
lcfl8b.v 
|- V = ( Base ` U )
lcfl8b.n 
|- N = ( LSpan ` U )
lcfl8b.z 
|- .0. = ( 0g ` U )
lcfl8b.f 
|- F = ( LFnl ` U )
lcfl8b.l 
|- L = ( LKer ` U )
lcfl8b.d 
|- D = ( LDual ` U )
lcfl8b.y 
|- Y = ( 0g ` D )
lcfl8b.c 
|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
lcfl8b.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfl8b.g 
|- ( ph -> G e. ( C \ { Y } ) )
Assertion lcfl8b 
|- ( ph -> E. x e. ( V \ { .0. } ) ( ._|_ ` ( L ` G ) ) = ( N ` { x } ) )

Proof

Step Hyp Ref Expression
1 lcfl8b.h 
 |-  H = ( LHyp ` K )
2 lcfl8b.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfl8b.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfl8b.v 
 |-  V = ( Base ` U )
5 lcfl8b.n 
 |-  N = ( LSpan ` U )
6 lcfl8b.z 
 |-  .0. = ( 0g ` U )
7 lcfl8b.f 
 |-  F = ( LFnl ` U )
8 lcfl8b.l 
 |-  L = ( LKer ` U )
9 lcfl8b.d 
 |-  D = ( LDual ` U )
10 lcfl8b.y 
 |-  Y = ( 0g ` D )
11 lcfl8b.c 
 |-  C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
12 lcfl8b.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
13 lcfl8b.g 
 |-  ( ph -> G e. ( C \ { Y } ) )
14 13 eldifad 
 |-  ( ph -> G e. C )
15 11 lcfl1lem 
 |-  ( G e. C <-> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
16 15 simplbi 
 |-  ( G e. C -> G e. F )
17 14 16 syl 
 |-  ( ph -> G e. F )
18 1 2 3 4 7 8 11 12 17 lcfl8 
 |-  ( ph -> ( G e. C <-> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) ) )
19 14 18 mpbid 
 |-  ( ph -> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) )
20 fveq2 
 |-  ( ( L ` G ) = ( ._|_ ` { x } ) -> ( ._|_ ` ( L ` G ) ) = ( ._|_ ` ( ._|_ ` { x } ) ) )
21 20 adantl 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ._|_ ` ( L ` G ) ) = ( ._|_ ` ( ._|_ ` { x } ) ) )
22 12 ad2antrr 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( K e. HL /\ W e. H ) )
23 simplr 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> x e. V )
24 1 3 2 4 5 22 23 dochocsn 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ._|_ ` ( ._|_ ` { x } ) ) = ( N ` { x } ) )
25 21 24 eqtrd 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ._|_ ` ( L ` G ) ) = ( N ` { x } ) )
26 14 15 sylib 
 |-  ( ph -> ( G e. F /\ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
27 26 simprd 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
28 eldifsni 
 |-  ( G e. ( C \ { Y } ) -> G =/= Y )
29 13 28 syl 
 |-  ( ph -> G =/= Y )
30 1 3 12 dvhlmod 
 |-  ( ph -> U e. LMod )
31 4 7 8 9 10 30 17 lkr0f2 
 |-  ( ph -> ( ( L ` G ) = V <-> G = Y ) )
32 31 necon3bid 
 |-  ( ph -> ( ( L ` G ) =/= V <-> G =/= Y ) )
33 29 32 mpbird 
 |-  ( ph -> ( L ` G ) =/= V )
34 27 33 eqnetrd 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )
35 34 ad2antrr 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )
36 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
37 17 ad2antrr 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> G e. F )
38 1 2 3 4 36 7 8 22 37 dochkrsat2 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) )
39 35 38 mpbid 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) )
40 25 39 eqeltrrd 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( N ` { x } ) e. ( LSAtoms ` U ) )
41 30 ad2antrr 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> U e. LMod )
42 4 5 6 36 41 23 lsatspn0 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ( N ` { x } ) e. ( LSAtoms ` U ) <-> x =/= .0. ) )
43 40 42 mpbid 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> x =/= .0. )
44 43 25 jca 
 |-  ( ( ( ph /\ x e. V ) /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( x =/= .0. /\ ( ._|_ ` ( L ` G ) ) = ( N ` { x } ) ) )
45 44 ex 
 |-  ( ( ph /\ x e. V ) -> ( ( L ` G ) = ( ._|_ ` { x } ) -> ( x =/= .0. /\ ( ._|_ ` ( L ` G ) ) = ( N ` { x } ) ) ) )
46 45 reximdva 
 |-  ( ph -> ( E. x e. V ( L ` G ) = ( ._|_ ` { x } ) -> E. x e. V ( x =/= .0. /\ ( ._|_ ` ( L ` G ) ) = ( N ` { x } ) ) ) )
47 19 46 mpd 
 |-  ( ph -> E. x e. V ( x =/= .0. /\ ( ._|_ ` ( L ` G ) ) = ( N ` { x } ) ) )
48 rexdifsn 
 |-  ( E. x e. ( V \ { .0. } ) ( ._|_ ` ( L ` G ) ) = ( N ` { x } ) <-> E. x e. V ( x =/= .0. /\ ( ._|_ ` ( L ` G ) ) = ( N ` { x } ) ) )
49 47 48 sylibr 
 |-  ( ph -> E. x e. ( V \ { .0. } ) ( ._|_ ` ( L ` G ) ) = ( N ` { x } ) )