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 )