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 ) ) ) |
| 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 ) ) ) |