Theorem dochsnkrlem2

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. } ) )
	dochsnkr.a	|- A = ( LSAtoms ` U )
Assertion	dochsnkrlem2	|- ( ph -> ( ._|_ ` ( L ` G ) ) e. A )

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		dochsnkr.a	|- A = ( LSAtoms ` U )
12	1 2 3 4 5 6 7 8 9 10	dochsnkrlem1	|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )
13	1 2 3 4 11 6 7 8 9	dochkrsat2	|- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V <-> ( ._|_ ` ( L ` G ) ) e. A ) )
14	12 13	mpbid	|- ( ph -> ( ._|_ ` ( L ` G ) ) e. A )