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
|- .+ = ( +g ` U )
lcf1o.t
|- .x. = ( .s ` U )
lcf1o.s
|- S = ( Scalar ` U )
lcf1o.r
|- R = ( Base ` S )
lcf1o.z
|- .0. = ( 0g ` U )
lcf1o.f
|- F = ( LFnl ` U )
lcf1o.l
|- L = ( LKer ` U )
lcf1o.d
|- D = ( LDual ` U )
lcf1o.q
|- Q = ( 0g ` D )
lcf1o.c
|- C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
lcf1o.j
|- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
lcflo.k
|- ( ph -> ( K e. HL /\ W e. H ) )
lcfrlem10.x
|- ( ph -> X e. ( V \ { .0. } ) )
Assertion lcfrlem15
|- ( ph -> X e. ( ._|_ ` ( 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
 |-  .+ = ( +g ` U )
6 lcf1o.t
 |-  .x. = ( .s ` U )
7 lcf1o.s
 |-  S = ( Scalar ` U )
8 lcf1o.r
 |-  R = ( Base ` S )
9 lcf1o.z
 |-  .0. = ( 0g ` U )
10 lcf1o.f
 |-  F = ( LFnl ` U )
11 lcf1o.l
 |-  L = ( LKer ` U )
12 lcf1o.d
 |-  D = ( LDual ` U )
13 lcf1o.q
 |-  Q = ( 0g ` D )
14 lcf1o.c
 |-  C = { f e. F | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
15 lcf1o.j
 |-  J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
16 lcflo.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
17 lcfrlem10.x
 |-  ( ph -> X e. ( V \ { .0. } ) )
18 1 3 16 dvhlmod
 |-  ( ph -> U e. LMod )
19 17 eldifad
 |-  ( ph -> X e. V )
20 eqid
 |-  ( LSpan ` U ) = ( LSpan ` U )
21 4 20 lspsnid
 |-  ( ( U e. LMod /\ X e. V ) -> X e. ( ( LSpan ` U ) ` { X } ) )
22 18 19 21 syl2anc
 |-  ( ph -> X e. ( ( LSpan ` U ) ` { X } ) )
23 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 20 lcfrlem14
 |-  ( ph -> ( ._|_ ` ( L ` ( J ` X ) ) ) = ( ( LSpan ` U ) ` { X } ) )
24 22 23 eleqtrrd
 |-  ( ph -> X e. ( ._|_ ` ( L ` ( J ` X ) ) ) )