Metamath Proof Explorer

Theorem lcfl9a

Description: Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015)

Ref Expression
Hypotheses lcfl9a.h 
|- H = ( LHyp ` K )
lcfl9a.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lcfl9a.u 
|- U = ( ( DVecH ` K ) ` W )
lcfl9a.v 
|- V = ( Base ` U )
lcfl9a.f 
|- F = ( LFnl ` U )
lcfl9a.l 
|- L = ( LKer ` U )
lcfl9a.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfl9a.g 
|- ( ph -> G e. F )
lcfl9a.x 
|- ( ph -> X e. V )
lcfl9a.s 
|- ( ph -> ( ._|_ ` { X } ) C_ ( L ` G ) )
Assertion lcfl9a 
|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )

Proof

Step Hyp Ref Expression
1 lcfl9a.h 
 |-  H = ( LHyp ` K )
2 lcfl9a.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfl9a.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfl9a.v 
 |-  V = ( Base ` U )
5 lcfl9a.f 
 |-  F = ( LFnl ` U )
6 lcfl9a.l 
 |-  L = ( LKer ` U )
7 lcfl9a.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 lcfl9a.g 
 |-  ( ph -> G e. F )
9 lcfl9a.x 
 |-  ( ph -> X e. V )
10 lcfl9a.s 
 |-  ( ph -> ( ._|_ ` { X } ) C_ ( L ` G ) )
11 1 3 2 4 7 dochoc1 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` V ) ) = V )
12 11 adantr 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( ._|_ ` ( ._|_ ` V ) ) = V )
13 1 3 7 dvhlmod 
 |-  ( ph -> U e. LMod )
14 4 5 6 13 8 lkrssv 
 |-  ( ph -> ( L ` G ) C_ V )
15 14 adantr 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( L ` G ) C_ V )
16 sneq 
 |-  ( X = ( 0g ` U ) -> { X } = { ( 0g ` U ) } )
17 16 fveq2d 
 |-  ( X = ( 0g ` U ) -> ( ._|_ ` { X } ) = ( ._|_ ` { ( 0g ` U ) } ) )
18 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
19 1 3 2 4 18 doch0 
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` { ( 0g ` U ) } ) = V )
20 7 19 syl 
 |-  ( ph -> ( ._|_ ` { ( 0g ` U ) } ) = V )
21 17 20 sylan9eqr 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( ._|_ ` { X } ) = V )
22 10 adantr 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( ._|_ ` { X } ) C_ ( L ` G ) )
23 21 22 eqsstrrd 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> V C_ ( L ` G ) )
24 15 23 eqssd 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( L ` G ) = V )
25 24 fveq2d 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( ._|_ ` ( L ` G ) ) = ( ._|_ ` V ) )
26 25 fveq2d 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( ._|_ ` ( ._|_ ` V ) ) )
27 12 26 24 3eqtr4d 
 |-  ( ( ph /\ X = ( 0g ` U ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
28 11 adantr 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( ._|_ ` ( ._|_ ` V ) ) = V )
29 simpr 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( L ` G ) = V )
30 29 fveq2d 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( ._|_ ` ( L ` G ) ) = ( ._|_ ` V ) )
31 30 fveq2d 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( ._|_ ` ( ._|_ ` V ) ) )
32 28 31 29 3eqtr4d 
 |-  ( ( ph /\ ( L ` G ) = V ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
33 9 snssd 
 |-  ( ph -> { X } C_ V )
34 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
35 1 34 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { X } C_ V ) -> ( ._|_ ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
36 7 33 35 syl2anc 
 |-  ( ph -> ( ._|_ ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
37 1 34 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { X } ) ) ) = ( ._|_ ` { X } ) )
38 7 36 37 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { X } ) ) ) = ( ._|_ ` { X } ) )
39 38 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { X } ) ) ) = ( ._|_ ` { X } ) )
40 10 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( ._|_ ` { X } ) C_ ( L ` G ) )
41 eqid 
 |-  ( LSHyp ` U ) = ( LSHyp ` U )
42 1 3 7 dvhlvec 
 |-  ( ph -> U e. LVec )
43 42 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> U e. LVec )
44 7 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( K e. HL /\ W e. H ) )
45 9 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> X e. V )
46 simprl 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> X =/= ( 0g ` U ) )
47 eldifsn 
 |-  ( X e. ( V \ { ( 0g ` U ) } ) <-> ( X e. V /\ X =/= ( 0g ` U ) ) )
48 45 46 47 sylanbrc 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> X e. ( V \ { ( 0g ` U ) } ) )
49 1 2 3 4 18 41 44 48 dochsnshp 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( ._|_ ` { X } ) e. ( LSHyp ` U ) )
50 simprr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( L ` G ) =/= V )
51 4 41 5 6 42 8 lkrshp4 
 |-  ( ph -> ( ( L ` G ) =/= V <-> ( L ` G ) e. ( LSHyp ` U ) ) )
52 51 adantr 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( ( L ` G ) =/= V <-> ( L ` G ) e. ( LSHyp ` U ) ) )
53 50 52 mpbid 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( L ` G ) e. ( LSHyp ` U ) )
54 41 43 49 53 lshpcmp 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( ( ._|_ ` { X } ) C_ ( L ` G ) <-> ( ._|_ ` { X } ) = ( L ` G ) ) )
55 40 54 mpbid 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( ._|_ ` { X } ) = ( L ` G ) )
56 55 fveq2d 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( ._|_ ` ( ._|_ ` { X } ) ) = ( ._|_ ` ( L ` G ) ) )
57 56 fveq2d 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { X } ) ) ) = ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) )
58 39 57 55 3eqtr3d 
 |-  ( ( ph /\ ( X =/= ( 0g ` U ) /\ ( L ` G ) =/= V ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
59 27 32 58 pm2.61da2ne 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )