Metamath Proof Explorer


Theorem lcfrlem16

Description: Lemma for lcfr . (Contributed by NM, 8-Mar-2015)

Ref Expression
Hypotheses lcf1o.h H = LHyp K
lcf1o.o ˙ = ocH K W
lcf1o.u U = DVecH K W
lcf1o.v V = Base U
lcf1o.a + ˙ = + U
lcf1o.t · ˙ = U
lcf1o.s S = Scalar U
lcf1o.r R = Base S
lcf1o.z 0 ˙ = 0 U
lcf1o.f F = LFnl U
lcf1o.l L = LKer U
lcf1o.d D = LDual U
lcf1o.q Q = 0 D
lcf1o.c C = f F | ˙ ˙ L f = L f
lcf1o.j J = x V 0 ˙ v V ι k R | w ˙ x v = w + ˙ k · ˙ x
lcflo.k φ K HL W H
lcfrlem16.p P = LSubSp D
lcfrlem16.g φ G P
lcfrlem16.gs φ G C
lcfrlem16.m E = g G ˙ L g
lcfrlem16.x φ X E 0 ˙
Assertion lcfrlem16 φ J X G

Proof

Step Hyp Ref Expression
1 lcf1o.h H = LHyp K
2 lcf1o.o ˙ = ocH K W
3 lcf1o.u U = DVecH K W
4 lcf1o.v V = Base U
5 lcf1o.a + ˙ = + U
6 lcf1o.t · ˙ = U
7 lcf1o.s S = Scalar U
8 lcf1o.r R = Base S
9 lcf1o.z 0 ˙ = 0 U
10 lcf1o.f F = LFnl U
11 lcf1o.l L = LKer U
12 lcf1o.d D = LDual U
13 lcf1o.q Q = 0 D
14 lcf1o.c C = f F | ˙ ˙ L f = L f
15 lcf1o.j J = x V 0 ˙ v V ι k R | w ˙ x v = w + ˙ k · ˙ x
16 lcflo.k φ K HL W H
17 lcfrlem16.p P = LSubSp D
18 lcfrlem16.g φ G P
19 lcfrlem16.gs φ G C
20 lcfrlem16.m E = g G ˙ L g
21 lcfrlem16.x φ X E 0 ˙
22 21 eldifad φ X E
23 22 20 eleqtrdi φ X g G ˙ L g
24 eliun X g G ˙ L g g G X ˙ L g
25 23 24 sylib φ g G X ˙ L g
26 eqid D = D
27 1 3 16 dvhlvec φ U LVec
28 27 3ad2ant1 φ g G X ˙ L g U LVec
29 eqid Base D = Base D
30 29 17 lssel G P g G g Base D
31 18 30 sylan φ g G g Base D
32 1 3 16 dvhlmod φ U LMod
33 10 12 29 32 ldualvbase φ Base D = F
34 33 adantr φ g G Base D = F
35 31 34 eleqtrd φ g G g F
36 35 3adant3 φ g G X ˙ L g g F
37 16 adantr φ g G K HL W H
38 32 adantr φ g G U LMod
39 4 10 11 38 35 lkrssv φ g G L g V
40 1 3 4 2 dochssv K HL W H L g V ˙ L g V
41 37 39 40 syl2anc φ g G ˙ L g V
42 41 ralrimiva φ g G ˙ L g V
43 iunss g G ˙ L g V g G ˙ L g V
44 42 43 sylibr φ g G ˙ L g V
45 20 44 eqsstrid φ E V
46 45 ssdifd φ E 0 ˙ V 0 ˙
47 46 21 sseldd φ X V 0 ˙
48 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47 lcfrlem10 φ J X F
49 48 3ad2ant1 φ g G X ˙ L g J X F
50 eqid LSAtoms U = LSAtoms U
51 16 3ad2ant1 φ g G X ˙ L g K HL W H
52 simp3 φ g G X ˙ L g X ˙ L g
53 eldifsni X E 0 ˙ X 0 ˙
54 21 53 syl φ X 0 ˙
55 54 3ad2ant1 φ g G X ˙ L g X 0 ˙
56 eldifsn X ˙ L g 0 ˙ X ˙ L g X 0 ˙
57 52 55 56 sylanbrc φ g G X ˙ L g X ˙ L g 0 ˙
58 1 2 3 4 9 10 11 51 36 57 50 dochsnkrlem2 φ g G X ˙ L g ˙ L g LSAtoms U
59 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47 lcfrlem15 φ X ˙ L J X
60 eldifsn X ˙ L J X 0 ˙ X ˙ L J X X 0 ˙
61 59 54 60 sylanbrc φ X ˙ L J X 0 ˙
62 1 2 3 4 9 10 11 16 48 61 50 dochsnkrlem2 φ ˙ L J X LSAtoms U
63 62 3ad2ant1 φ g G X ˙ L g ˙ L J X LSAtoms U
64 59 3ad2ant1 φ g G X ˙ L g X ˙ L J X
65 9 50 28 58 63 55 52 64 lsat2el φ g G X ˙ L g ˙ L g = ˙ L J X
66 eqid DIsoH K W = DIsoH K W
67 19 3ad2ant1 φ g G X ˙ L g G C
68 simp2 φ g G X ˙ L g g G
69 67 68 sseldd φ g G X ˙ L g g C
70 1 66 2 3 10 11 14 51 36 lcfl5 φ g G X ˙ L g g C L g ran DIsoH K W
71 69 70 mpbid φ g G X ˙ L g L g ran DIsoH K W
72 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47 lcfrlem13 φ J X C Q
73 72 eldifad φ J X C
74 1 66 2 3 10 11 14 16 48 lcfl5 φ J X C L J X ran DIsoH K W
75 73 74 mpbid φ L J X ran DIsoH K W
76 75 3ad2ant1 φ g G X ˙ L g L J X ran DIsoH K W
77 1 66 2 51 71 76 doch11 φ g G X ˙ L g ˙ L g = ˙ L J X L g = L J X
78 65 77 mpbid φ g G X ˙ L g L g = L J X
79 7 8 10 11 12 26 28 36 49 78 eqlkr4 φ g G X ˙ L g k R J X = k D g
80 32 3ad2ant1 φ g G X ˙ L g U LMod
81 80 adantr φ g G X ˙ L g k R U LMod
82 18 3ad2ant1 φ g G X ˙ L g G P
83 82 adantr φ g G X ˙ L g k R G P
84 simpr φ g G X ˙ L g k R k R
85 simpl2 φ g G X ˙ L g k R g G
86 7 8 12 26 17 81 83 84 85 ldualssvscl φ g G X ˙ L g k R k D g G
87 eleq1 J X = k D g J X G k D g G
88 86 87 syl5ibrcom φ g G X ˙ L g k R J X = k D g J X G
89 88 rexlimdva φ g G X ˙ L g k R J X = k D g J X G
90 79 89 mpd φ g G X ˙ L g J X G
91 90 rexlimdv3a φ g G X ˙ L g J X G
92 25 91 mpd φ J X G