Metamath Proof Explorer

Theorem lcfl6

Description: Property of a functional with a closed kernel. Note that ( LG ) = V means the functional is zero by lkr0f . (Contributed by NM, 3-Jan-2015)

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

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 df-ne 
 |-  ( ( L ` G ) =/= V <-> -. ( L ` G ) = V )
16 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
17 13 ad2antrr 
 |-  ( ( ( ph /\ G e. C ) /\ ( L ` G ) =/= V ) -> ( K e. HL /\ W e. H ) )
18 14 ad2antrr 
 |-  ( ( ( ph /\ G e. C ) /\ ( L ` G ) =/= V ) -> G e. F )
19 1 2 3 4 10 11 12 13 14 lcfl2 
 |-  ( ph -> ( G e. C <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V \/ ( L ` G ) = V ) ) )
20 19 biimpa 
 |-  ( ( ph /\ G e. C ) -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V \/ ( L ` G ) = V ) )
21 20 orcomd 
 |-  ( ( ph /\ G e. C ) -> ( ( L ` G ) = V \/ ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V ) )
22 21 ord 
 |-  ( ( ph /\ G e. C ) -> ( -. ( L ` G ) = V -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V ) )
23 15 22 syl5bi 
 |-  ( ( ph /\ G e. C ) -> ( ( L ` G ) =/= V -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V ) )
24 23 imp 
 |-  ( ( ( ph /\ G e. C ) /\ ( L ` G ) =/= V ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )
25 1 2 3 4 7 9 16 10 11 17 18 24 dochkr1 
 |-  ( ( ( ph /\ G e. C ) /\ ( L ` G ) =/= V ) -> E. x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) ( G ` x ) = ( 1r ` S ) )
26 1 3 13 dvhlmod 
 |-  ( ph -> U e. LMod )
27 4 10 11 26 14 lkrssv 
 |-  ( ph -> ( L ` G ) C_ V )
28 1 3 4 2 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( L ` G ) C_ V ) -> ( ._|_ ` ( L ` G ) ) C_ V )
29 13 27 28 syl2anc 
 |-  ( ph -> ( ._|_ ` ( L ` G ) ) C_ V )
30 29 ssdifd 
 |-  ( ph -> ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) C_ ( V \ { .0. } ) )
31 30 ad3antrrr 
 |-  ( ( ( ( ph /\ G e. C ) /\ ( L ` G ) =/= V ) /\ ( x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) /\ ( G ` x ) = ( 1r ` S ) ) ) -> ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) C_ ( V \ { .0. } ) )
32 simprl 
 |-  ( ( ( ( ph /\ G e. C ) /\ ( L ` G ) =/= V ) /\ ( x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) /\ ( G ` x ) = ( 1r ` S ) ) ) -> x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )
33 31 32 sseldd 
 |-  ( ( ( ( ph /\ G e. C ) /\ ( L ` G ) =/= V ) /\ ( x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) /\ ( G ` x ) = ( 1r ` S ) ) ) -> x e. ( V \ { .0. } ) )
34 13 ad3antrrr 
 |-  ( ( ( ( ph /\ G e. C ) /\ ( L ` G ) =/= V ) /\ ( x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) /\ ( G ` x ) = ( 1r ` S ) ) ) -> ( K e. HL /\ W e. H ) )
35 14 ad3antrrr 
 |-  ( ( ( ( ph /\ G e. C ) /\ ( L ` G ) =/= V ) /\ ( x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) /\ ( G ` x ) = ( 1r ` S ) ) ) -> G e. F )
36 simprr 
 |-  ( ( ( ( ph /\ G e. C ) /\ ( L ` G ) =/= V ) /\ ( x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) /\ ( G ` x ) = ( 1r ` S ) ) ) -> ( G ` x ) = ( 1r ` S ) )
37 1 2 3 4 5 6 7 16 8 9 10 11 34 35 32 36 lcfl6lem 
 |-  ( ( ( ( ph /\ G e. C ) /\ ( L ` G ) =/= V ) /\ ( x e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) /\ ( G ` x ) = ( 1r ` S ) ) ) -> G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
38 25 33 37 reximssdv 
 |-  ( ( ( 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 ) ) ) ) )
39 38 ex 
 |-  ( ( 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 ) ) ) ) ) )
40 15 39 syl5bir 
 |-  ( ( 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 ) ) ) ) ) )
41 40 orrd 
 |-  ( ( 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 ) ) ) ) ) )
42 41 ex 
 |-  ( 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 ) ) ) ) ) ) )
43 olc 
 |-  ( ( L ` G ) = V -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V \/ ( L ` G ) = V ) )
44 43 19 syl5ibr 
 |-  ( ph -> ( ( L ` G ) = V -> G e. C ) )
45 13 adantr 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> ( K e. HL /\ W e. H ) )
46 eldifi 
 |-  ( x e. ( V \ { .0. } ) -> x e. V )
47 46 adantl 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> x e. V )
48 47 snssd 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> { x } C_ V )
49 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
50 1 49 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { x } C_ V ) -> ( ._|_ ` { x } ) e. ran ( ( DIsoH ` K ) ` W ) )
51 45 48 50 syl2anc 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> ( ._|_ ` { x } ) e. ran ( ( DIsoH ` K ) ` W ) )
52 1 49 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` { x } ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { x } ) ) ) = ( ._|_ ` { x } ) )
53 45 51 52 syl2anc 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { x } ) ) ) = ( ._|_ ` { x } ) )
54 53 3adant3 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { x } ) ) ) = ( ._|_ ` { x } ) )
55 simp3 
 |-  ( ( ph /\ x 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. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
56 55 fveq2d 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) -> ( L ` G ) = ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) )
57 eqid 
 |-  ( 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. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) )
58 simpr 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> x e. ( V \ { .0. } ) )
59 1 2 3 4 9 5 6 11 7 8 57 45 58 dochsnkr2 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) ) -> ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) = ( ._|_ ` { x } ) )
60 59 3adant3 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) -> ( L ` ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) = ( ._|_ ` { x } ) )
61 56 60 eqtrd 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) -> ( L ` G ) = ( ._|_ ` { x } ) )
62 61 fveq2d 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) -> ( ._|_ ` ( L ` G ) ) = ( ._|_ ` ( ._|_ ` { x } ) ) )
63 62 fveq2d 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( ._|_ ` ( ._|_ ` ( ._|_ ` { x } ) ) ) )
64 54 63 61 3eqtr4d 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
65 14 3ad2ant1 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) -> G e. F )
66 12 65 lcfl1 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) -> ( G e. C <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
67 64 66 mpbird 
 |-  ( ( ph /\ x e. ( V \ { .0. } ) /\ G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) ) -> G e. C )
68 67 rexlimdv3a 
 |-  ( ph -> ( E. x e. ( V \ { .0. } ) G = ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) -> G e. C ) )
69 44 68 jaod 
 |-  ( 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 ) ) ) ) ) -> G e. C ) )
70 42 69 impbid 
 |-  ( 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 ) ) ) ) ) ) )