# Metamath Proof Explorer

## Theorem dochsnkrlem1

Description: Lemma for dochsnkr . (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochsnkr.h
`|- H = ( LHyp ` K )`
dochsnkr.o
`|- ._|_ = ( ( ocH ` K ) ` W )`
dochsnkr.u
`|- U = ( ( DVecH ` K ) ` W )`
dochsnkr.v
`|- V = ( Base ` U )`
dochsnkr.z
`|- .0. = ( 0g ` U )`
dochsnkr.f
`|- F = ( LFnl ` U )`
dochsnkr.l
`|- L = ( LKer ` U )`
dochsnkr.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
dochsnkr.g
`|- ( ph -> G e. F )`
dochsnkr.x
`|- ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )`
Assertion dochsnkrlem1
`|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )`

### Proof

Step Hyp Ref Expression
1 dochsnkr.h
` |-  H = ( LHyp ` K )`
2 dochsnkr.o
` |-  ._|_ = ( ( ocH ` K ) ` W )`
3 dochsnkr.u
` |-  U = ( ( DVecH ` K ) ` W )`
4 dochsnkr.v
` |-  V = ( Base ` U )`
5 dochsnkr.z
` |-  .0. = ( 0g ` U )`
6 dochsnkr.f
` |-  F = ( LFnl ` U )`
7 dochsnkr.l
` |-  L = ( LKer ` U )`
8 dochsnkr.k
` |-  ( ph -> ( K e. HL /\ W e. H ) )`
9 dochsnkr.g
` |-  ( ph -> G e. F )`
10 dochsnkr.x
` |-  ( ph -> X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) )`
11 eldif
` |-  ( X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) <-> ( X e. ( ._|_ ` ( L ` G ) ) /\ -. X e. { .0. } ) )`
12 nelne1
` |-  ( ( X e. ( ._|_ ` ( L ` G ) ) /\ -. X e. { .0. } ) -> ( ._|_ ` ( L ` G ) ) =/= { .0. } )`
13 11 12 sylbi
` |-  ( X e. ( ( ._|_ ` ( L ` G ) ) \ { .0. } ) -> ( ._|_ ` ( L ` G ) ) =/= { .0. } )`
14 10 13 syl
` |-  ( ph -> ( ._|_ ` ( L ` G ) ) =/= { .0. } )`
15 1 3 8 dvhlmod
` |-  ( ph -> U e. LMod )`
16 4 6 7 15 9 lkrssv
` |-  ( ph -> ( L ` G ) C_ V )`
17 1 2 3 4 5 8 16 dochn0nv
` |-  ( ph -> ( ( ._|_ ` ( L ` G ) ) =/= { .0. } <-> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V ) )`
18 14 17 mpbid
` |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )`