Metamath Proof Explorer

Theorem lcfl8

Description: Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 lcfl8.h 
 |-  H = ( LHyp ` K )
2 lcfl8.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lcfl8.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lcfl8.v 
 |-  V = ( Base ` U )
5 lcfl8.f 
 |-  F = ( LFnl ` U )
6 lcfl8.l 
 |-  L = ( LKer ` U )
7 lcfl8.c 
 |-  C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
8 lcfl8.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 lcfl8.g 
 |-  ( ph -> G e. F )
10 1 3 8 dvhlmod 
 |-  ( ph -> U e. LMod )
11 10 adantr 
 |-  ( ( ph /\ G e. C ) -> U e. LMod )
12 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
13 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
14 4 12 13 islsati 
 |-  ( ( U e. LMod /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) -> E. x e. V ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) )
15 11 14 sylan 
 |-  ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) -> E. x e. V ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) )
16 simpr 
 |-  ( ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) /\ ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) ) -> ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) )
17 16 fveq2d 
 |-  ( ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) /\ ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( ._|_ ` ( ( LSpan ` U ) ` { x } ) ) )
18 simp-4r 
 |-  ( ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) /\ ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) ) -> G e. C )
19 9 ad4antr 
 |-  ( ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) /\ ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) ) -> G e. F )
20 7 19 lcfl1 
 |-  ( ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) /\ ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) ) -> ( G e. C <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
21 18 20 mpbid 
 |-  ( ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) /\ ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
22 8 ad4antr 
 |-  ( ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) /\ ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) ) -> ( K e. HL /\ W e. H ) )
23 simplr 
 |-  ( ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) /\ ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) ) -> x e. V )
24 23 snssd 
 |-  ( ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) /\ ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) ) -> { x } C_ V )
25 1 3 2 4 12 22 24 dochocsp 
 |-  ( ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) /\ ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) ) -> ( ._|_ ` ( ( LSpan ` U ) ` { x } ) ) = ( ._|_ ` { x } ) )
26 17 21 25 3eqtr3d 
 |-  ( ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) /\ ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) ) -> ( L ` G ) = ( ._|_ ` { x } ) )
27 26 ex 
 |-  ( ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) /\ x e. V ) -> ( ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) -> ( L ` G ) = ( ._|_ ` { x } ) ) )
28 27 reximdva 
 |-  ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) -> ( E. x e. V ( ._|_ ` ( L ` G ) ) = ( ( LSpan ` U ) ` { x } ) -> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) ) )
29 15 28 mpd 
 |-  ( ( ( ph /\ G e. C ) /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) -> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) )
30 11 adantr 
 |-  ( ( ( ph /\ G e. C ) /\ ( L ` G ) = V ) -> U e. LMod )
31 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
32 4 31 lmod0vcl 
 |-  ( U e. LMod -> ( 0g ` U ) e. V )
33 30 32 syl 
 |-  ( ( ( ph /\ G e. C ) /\ ( L ` G ) = V ) -> ( 0g ` U ) e. V )
34 simpr 
 |-  ( ( ( ph /\ G e. C ) /\ ( L ` G ) = V ) -> ( L ` G ) = V )
35 8 adantr 
 |-  ( ( ph /\ G e. C ) -> ( K e. HL /\ W e. H ) )
36 35 adantr 
 |-  ( ( ( ph /\ G e. C ) /\ ( L ` G ) = V ) -> ( K e. HL /\ W e. H ) )
37 1 3 2 4 31 doch0 
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` { ( 0g ` U ) } ) = V )
38 36 37 syl 
 |-  ( ( ( ph /\ G e. C ) /\ ( L ` G ) = V ) -> ( ._|_ ` { ( 0g ` U ) } ) = V )
39 34 38 eqtr4d 
 |-  ( ( ( ph /\ G e. C ) /\ ( L ` G ) = V ) -> ( L ` G ) = ( ._|_ ` { ( 0g ` U ) } ) )
40 sneq 
 |-  ( x = ( 0g ` U ) -> { x } = { ( 0g ` U ) } )
41 40 fveq2d 
 |-  ( x = ( 0g ` U ) -> ( ._|_ ` { x } ) = ( ._|_ ` { ( 0g ` U ) } ) )
42 41 rspceeqv 
 |-  ( ( ( 0g ` U ) e. V /\ ( L ` G ) = ( ._|_ ` { ( 0g ` U ) } ) ) -> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) )
43 33 39 42 syl2anc 
 |-  ( ( ( ph /\ G e. C ) /\ ( L ` G ) = V ) -> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) )
44 1 2 3 4 13 5 6 7 8 9 lcfl3 
 |-  ( ph -> ( G e. C <-> ( ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) \/ ( L ` G ) = V ) ) )
45 44 biimpa 
 |-  ( ( ph /\ G e. C ) -> ( ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) \/ ( L ` G ) = V ) )
46 29 43 45 mpjaodan 
 |-  ( ( ph /\ G e. C ) -> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) )
47 46 ex 
 |-  ( ph -> ( G e. C -> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) ) )
48 8 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( K e. HL /\ W e. H ) )
49 simp2 
 |-  ( ( ph /\ x e. V /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> x e. V )
50 49 snssd 
 |-  ( ( ph /\ x e. V /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> { x } C_ V )
51 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
52 1 51 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { x } C_ V ) -> ( ._|_ ` { x } ) e. ran ( ( DIsoH ` K ) ` W ) )
53 48 50 52 syl2anc 
 |-  ( ( ph /\ x e. V /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ._|_ ` { x } ) e. ran ( ( DIsoH ` K ) ` W ) )
54 1 51 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` { x } ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { x } ) ) ) = ( ._|_ ` { x } ) )
55 48 53 54 syl2anc 
 |-  ( ( ph /\ x e. V /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { x } ) ) ) = ( ._|_ ` { x } ) )
56 simp3 
 |-  ( ( ph /\ x e. V /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( L ` G ) = ( ._|_ ` { x } ) )
57 56 fveq2d 
 |-  ( ( ph /\ x e. V /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ._|_ ` ( L ` G ) ) = ( ._|_ ` ( ._|_ ` { x } ) ) )
58 57 fveq2d 
 |-  ( ( ph /\ x e. V /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( ._|_ ` ( ._|_ ` ( ._|_ ` { x } ) ) ) )
59 55 58 56 3eqtr4d 
 |-  ( ( ph /\ x e. V /\ ( L ` G ) = ( ._|_ ` { x } ) ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )
60 59 rexlimdv3a 
 |-  ( ph -> ( E. x e. V ( L ` G ) = ( ._|_ ` { x } ) -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
61 7 9 lcfl1 
 |-  ( ph -> ( G e. C <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) ) )
62 60 61 sylibrd 
 |-  ( ph -> ( E. x e. V ( L ` G ) = ( ._|_ ` { x } ) -> G e. C ) )
63 47 62 impbid 
 |-  ( ph -> ( G e. C <-> E. x e. V ( L ` G ) = ( ._|_ ` { x } ) ) )