Metamath Proof Explorer


Theorem lclkrlem2w

Description: Lemma for lclkr . This is the same as lclkrlem2u and lclkrlem2u with the inequality hypotheses negated. When the sum of two functionals is zero at each generating vector, the kernel is the vector space and therefore closed. (Contributed by NM, 16-Jan-2015)

Ref Expression
Hypotheses lclkrlem2m.v
|- V = ( Base ` U )
lclkrlem2m.t
|- .x. = ( .s ` U )
lclkrlem2m.s
|- S = ( Scalar ` U )
lclkrlem2m.q
|- .X. = ( .r ` S )
lclkrlem2m.z
|- .0. = ( 0g ` S )
lclkrlem2m.i
|- I = ( invr ` S )
lclkrlem2m.m
|- .- = ( -g ` U )
lclkrlem2m.f
|- F = ( LFnl ` U )
lclkrlem2m.d
|- D = ( LDual ` U )
lclkrlem2m.p
|- .+ = ( +g ` D )
lclkrlem2m.x
|- ( ph -> X e. V )
lclkrlem2m.y
|- ( ph -> Y e. V )
lclkrlem2m.e
|- ( ph -> E e. F )
lclkrlem2m.g
|- ( ph -> G e. F )
lclkrlem2n.n
|- N = ( LSpan ` U )
lclkrlem2n.l
|- L = ( LKer ` U )
lclkrlem2o.h
|- H = ( LHyp ` K )
lclkrlem2o.o
|- ._|_ = ( ( ocH ` K ) ` W )
lclkrlem2o.u
|- U = ( ( DVecH ` K ) ` W )
lclkrlem2o.a
|- .(+) = ( LSSum ` U )
lclkrlem2o.k
|- ( ph -> ( K e. HL /\ W e. H ) )
lclkrlem2q.le
|- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )
lclkrlem2q.lg
|- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )
lclkrlem2v.j
|- ( ph -> ( ( E .+ G ) ` X ) = .0. )
lclkrlem2v.k
|- ( ph -> ( ( E .+ G ) ` Y ) = .0. )
Assertion lclkrlem2w
|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2m.v
 |-  V = ( Base ` U )
2 lclkrlem2m.t
 |-  .x. = ( .s ` U )
3 lclkrlem2m.s
 |-  S = ( Scalar ` U )
4 lclkrlem2m.q
 |-  .X. = ( .r ` S )
5 lclkrlem2m.z
 |-  .0. = ( 0g ` S )
6 lclkrlem2m.i
 |-  I = ( invr ` S )
7 lclkrlem2m.m
 |-  .- = ( -g ` U )
8 lclkrlem2m.f
 |-  F = ( LFnl ` U )
9 lclkrlem2m.d
 |-  D = ( LDual ` U )
10 lclkrlem2m.p
 |-  .+ = ( +g ` D )
11 lclkrlem2m.x
 |-  ( ph -> X e. V )
12 lclkrlem2m.y
 |-  ( ph -> Y e. V )
13 lclkrlem2m.e
 |-  ( ph -> E e. F )
14 lclkrlem2m.g
 |-  ( ph -> G e. F )
15 lclkrlem2n.n
 |-  N = ( LSpan ` U )
16 lclkrlem2n.l
 |-  L = ( LKer ` U )
17 lclkrlem2o.h
 |-  H = ( LHyp ` K )
18 lclkrlem2o.o
 |-  ._|_ = ( ( ocH ` K ) ` W )
19 lclkrlem2o.u
 |-  U = ( ( DVecH ` K ) ` W )
20 lclkrlem2o.a
 |-  .(+) = ( LSSum ` U )
21 lclkrlem2o.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
22 lclkrlem2q.le
 |-  ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )
23 lclkrlem2q.lg
 |-  ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )
24 lclkrlem2v.j
 |-  ( ph -> ( ( E .+ G ) ` X ) = .0. )
25 lclkrlem2v.k
 |-  ( ph -> ( ( E .+ G ) ` Y ) = .0. )
26 17 19 18 1 21 dochoc1
 |-  ( ph -> ( ._|_ ` ( ._|_ ` V ) ) = V )
27 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 lclkrlem2v
 |-  ( ph -> ( L ` ( E .+ G ) ) = V )
28 27 fveq2d
 |-  ( ph -> ( ._|_ ` ( L ` ( E .+ G ) ) ) = ( ._|_ ` V ) )
29 28 fveq2d
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( ._|_ ` ( ._|_ ` V ) ) )
30 26 29 27 3eqtr4d
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )