Metamath Proof Explorer


Theorem lcfrlem15

Description: Lemma for lcfr . (Contributed by NM, 9-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 ˙
Assertion lcfrlem15 φ X ˙ L J 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 1 3 16 dvhlmod φ U LMod
19 17 eldifad φ X V
20 eqid LSpan U = LSpan U
21 4 20 lspsnid U LMod X V X LSpan U X
22 18 19 21 syl2anc φ X LSpan U X
23 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 20 lcfrlem14 φ ˙ L J X = LSpan U X
24 22 23 eleqtrrd φ X ˙ L J X