Metamath Proof Explorer


Theorem lcfrlem14

Description: Lemma for lcfr . (Contributed by NM, 10-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
lcfrlem10.x φ X V 0 ˙
lcfrlem14.n N = LSpan U
Assertion lcfrlem14 φ ˙ L J X = N X

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 lcfrlem10.x φ X V 0 ˙
18 lcfrlem14.n N = LSpan U
19 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 lcfrlem11 φ L J X = ˙ X
20 17 eldifad φ X V
21 20 snssd φ X V
22 1 3 2 4 18 16 21 dochocsp φ ˙ N X = ˙ X
23 19 22 eqtr4d φ L J X = ˙ N X
24 23 fveq2d φ ˙ L J X = ˙ ˙ N X
25 eqid DIsoH K W = DIsoH K W
26 1 3 4 18 25 dihlsprn K HL W H X V N X ran DIsoH K W
27 16 20 26 syl2anc φ N X ran DIsoH K W
28 1 25 2 dochoc K HL W H N X ran DIsoH K W ˙ ˙ N X = N X
29 16 27 28 syl2anc φ ˙ ˙ N X = N X
30 24 29 eqtrd φ ˙ L J X = N X