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 F | ˙ ˙ L f = L f
lcfl8.k φ K HL W H
lcfl8.g φ G F
Assertion lcfl8 φ G C x 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 F | ˙ ˙ L f = L f
8 lcfl8.k φ K HL W H
9 lcfl8.g φ G F
10 1 3 8 dvhlmod φ U LMod
11 10 adantr φ G C U LMod
12 eqid LSpan U = LSpan U
13 eqid LSAtoms U = LSAtoms U
14 4 12 13 islsati U LMod ˙ L G LSAtoms U x V ˙ L G = LSpan U x
15 11 14 sylan φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x
16 simpr φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x ˙ L G = LSpan U x
17 16 fveq2d φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x ˙ ˙ L G = ˙ LSpan U x
18 simp-4r φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x G C
19 9 ad4antr φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x G F
20 7 19 lcfl1 φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x G C ˙ ˙ L G = L G
21 18 20 mpbid φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x ˙ ˙ L G = L G
22 8 ad4antr φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x K HL W H
23 simplr φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x x V
24 23 snssd φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x x V
25 1 3 2 4 12 22 24 dochocsp φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x ˙ LSpan U x = ˙ x
26 17 21 25 3eqtr3d φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x L G = ˙ x
27 26 ex φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x L G = ˙ x
28 27 reximdva φ G C ˙ L G LSAtoms U x V ˙ L G = LSpan U x x V L G = ˙ x
29 15 28 mpd φ G C ˙ L G LSAtoms U x V L G = ˙ x
30 11 adantr φ G C L G = V U LMod
31 eqid 0 U = 0 U
32 4 31 lmod0vcl U LMod 0 U V
33 30 32 syl φ G C L G = V 0 U V
34 simpr φ G C L G = V L G = V
35 8 adantr φ G C K HL W H
36 35 adantr φ G C L G = V K HL W H
37 1 3 2 4 31 doch0 K HL W H ˙ 0 U = V
38 36 37 syl φ G C L G = V ˙ 0 U = V
39 34 38 eqtr4d φ G C L G = V L G = ˙ 0 U
40 sneq x = 0 U x = 0 U
41 40 fveq2d x = 0 U ˙ x = ˙ 0 U
42 41 rspceeqv 0 U V L G = ˙ 0 U x V L G = ˙ x
43 33 39 42 syl2anc φ G C L G = V x V L G = ˙ x
44 1 2 3 4 13 5 6 7 8 9 lcfl3 φ G C ˙ L G LSAtoms U L G = V
45 44 biimpa φ G C ˙ L G LSAtoms U L G = V
46 29 43 45 mpjaodan φ G C x V L G = ˙ x
47 46 ex φ G C x V L G = ˙ x
48 8 3ad2ant1 φ x V L G = ˙ x K HL W H
49 simp2 φ x V L G = ˙ x x V
50 49 snssd φ x V L G = ˙ x x V
51 eqid DIsoH K W = DIsoH K W
52 1 51 3 4 2 dochcl K HL W H x V ˙ x ran DIsoH K W
53 48 50 52 syl2anc φ x V L G = ˙ x ˙ x ran DIsoH K W
54 1 51 2 dochoc K HL W H ˙ x ran DIsoH K W ˙ ˙ ˙ x = ˙ x
55 48 53 54 syl2anc φ x V L G = ˙ x ˙ ˙ ˙ x = ˙ x
56 simp3 φ x V L G = ˙ x L G = ˙ x
57 56 fveq2d φ x V L G = ˙ x ˙ L G = ˙ ˙ x
58 57 fveq2d φ x V L G = ˙ x ˙ ˙ L G = ˙ ˙ ˙ x
59 55 58 56 3eqtr4d φ x V L G = ˙ x ˙ ˙ L G = L G
60 59 rexlimdv3a φ x V L G = ˙ x ˙ ˙ L G = L G
61 7 9 lcfl1 φ G C ˙ ˙ L G = L G
62 60 61 sylibrd φ x V L G = ˙ x G C
63 47 62 impbid φ G C x V L G = ˙ x