Theorem dochsnkrlem3

Description: Lemma for dochsnkr . (Contributed by NM, 2-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	dochsnkrlem3	|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )

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	1 2 3 4 5 6 7 8 9 10	dochsnkrlem1	|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V )
12	11	orcd	|- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V \/ ( L ` G ) = V ) )
13	1 2 3 4 6 7 8 9	dochkrshp4	|- ( ph -> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) <-> ( ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) =/= V \/ ( L ` G ) = V ) ) )
14	12 13	mpbird	|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` G ) ) ) = ( L ` G ) )