Description: Lemma for lclkr . When B is zero, i.e. when X and Y are colinear, the intersection of the kernels of E and G equal the kernel of G , so the kernels of G and the sum are comparable. (Contributed by NM, 18-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 } ) ) |
||
| lclkrlem2q.b | |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) |
||
| lclkrlem2q.n | |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. ) |
||
| lclkrlem2r.bn | |- ( ph -> B = ( 0g ` U ) ) |
||
| Assertion | lclkrlem2r | |- ( ph -> ( L ` G ) C_ ( 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 | lclkrlem2q.b | |- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) |
|
| 25 | lclkrlem2q.n | |- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. ) |
|
| 26 | lclkrlem2r.bn | |- ( ph -> B = ( 0g ` U ) ) |
|
| 27 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 24 25 26 | lclkrlem2p | |- ( ph -> ( ._|_ ` { Y } ) C_ ( ._|_ ` { X } ) ) |
| 28 | 27 23 22 | 3sstr4d | |- ( ph -> ( L ` G ) C_ ( L ` E ) ) |
| 29 | sseqin2 | |- ( ( L ` G ) C_ ( L ` E ) <-> ( ( L ` E ) i^i ( L ` G ) ) = ( L ` G ) ) |
|
| 30 | 28 29 | sylib | |- ( ph -> ( ( L ` E ) i^i ( L ` G ) ) = ( L ` G ) ) |
| 31 | 17 19 21 | dvhlmod | |- ( ph -> U e. LMod ) |
| 32 | 8 16 9 10 31 13 14 | lkrin | |- ( ph -> ( ( L ` E ) i^i ( L ` G ) ) C_ ( L ` ( E .+ G ) ) ) |
| 33 | 30 32 | eqsstrrd | |- ( ph -> ( L ` G ) C_ ( L ` ( E .+ G ) ) ) |