Theorem lclkrlem2k

Description: Lemma for lclkr . Kernel closure when X is zero. (Contributed by NM, 18-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2f.h	|- H = ( LHyp ` K )
	lclkrlem2f.o	|- ._|_ = ( ( ocH ` K ) ` W )
	lclkrlem2f.u	|- U = ( ( DVecH ` K ) ` W )
	lclkrlem2f.v	|- V = ( Base ` U )
	lclkrlem2f.s	|- S = ( Scalar ` U )
	lclkrlem2f.q	|- Q = ( 0g ` S )
	lclkrlem2f.z	|- .0. = ( 0g ` U )
	lclkrlem2f.a	|- .(+) = ( LSSum ` U )
	lclkrlem2f.n	|- N = ( LSpan ` U )
	lclkrlem2f.f	|- F = ( LFnl ` U )
	lclkrlem2f.j	|- J = ( LSHyp ` U )
	lclkrlem2f.l	|- L = ( LKer ` U )
	lclkrlem2f.d	|- D = ( LDual ` U )
	lclkrlem2f.p	|- .+ = ( +g ` D )
	lclkrlem2f.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lclkrlem2f.b	|- ( ph -> B e. ( V \ { .0. } ) )
	lclkrlem2f.e	|- ( ph -> E e. F )
	lclkrlem2f.g	|- ( ph -> G e. F )
	lclkrlem2f.le	|- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )
	lclkrlem2f.lg	|- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )
	lclkrlem2f.kb	|- ( ph -> ( ( E .+ G ) ` B ) = Q )
	lclkrlem2f.nx	|- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )
	lclkrlem2k.x	|- ( ph -> X = .0. )
	lclkrlem2k.y	|- ( ph -> Y e. V )
Assertion	lclkrlem2k	|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2f.h	|- H = ( LHyp ` K )
2		lclkrlem2f.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		lclkrlem2f.u	|- U = ( ( DVecH ` K ) ` W )
4		lclkrlem2f.v	|- V = ( Base ` U )
5		lclkrlem2f.s	|- S = ( Scalar ` U )
6		lclkrlem2f.q	|- Q = ( 0g ` S )
7		lclkrlem2f.z	|- .0. = ( 0g ` U )
8		lclkrlem2f.a	|- .(+) = ( LSSum ` U )
9		lclkrlem2f.n	|- N = ( LSpan ` U )
10		lclkrlem2f.f	|- F = ( LFnl ` U )
11		lclkrlem2f.j	|- J = ( LSHyp ` U )
12		lclkrlem2f.l	|- L = ( LKer ` U )
13		lclkrlem2f.d	|- D = ( LDual ` U )
14		lclkrlem2f.p	|- .+ = ( +g ` D )
15		lclkrlem2f.k	|- ( ph -> ( K e. HL /\ W e. H ) )
16		lclkrlem2f.b	|- ( ph -> B e. ( V \ { .0. } ) )
17		lclkrlem2f.e	|- ( ph -> E e. F )
18		lclkrlem2f.g	|- ( ph -> G e. F )
19		lclkrlem2f.le	|- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )
20		lclkrlem2f.lg	|- ( ph -> ( L ` G ) = ( ._|_ ` { Y } ) )
21		lclkrlem2f.kb	|- ( ph -> ( ( E .+ G ) ` B ) = Q )
22		lclkrlem2f.nx	|- ( ph -> ( -. X e. ( ._|_ ` { B } ) \/ -. Y e. ( ._|_ ` { B } ) ) )
23		lclkrlem2k.x	|- ( ph -> X = .0. )
24		lclkrlem2k.y	|- ( ph -> Y e. V )
25	1 3 15	dvhlmod	|- ( ph -> U e. LMod )
26	10 13 14 25 17 18	ldualvaddcom	|- ( ph -> ( E .+ G ) = ( G .+ E ) )
27	26	fveq1d	|- ( ph -> ( ( E .+ G ) ` B ) = ( ( G .+ E ) ` B ) )
28	27 21	eqtr3d	|- ( ph -> ( ( G .+ E ) ` B ) = Q )
29	22	orcomd	|- ( ph -> ( -. Y e. ( ._|_ ` { B } ) \/ -. X e. ( ._|_ ` { B } ) ) )
30	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 18 17 20 19 28 29 24 23	lclkrlem2j	|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( G .+ E ) ) ) ) = ( L ` ( G .+ E ) ) )
31	26	fveq2d	|- ( ph -> ( L ` ( E .+ G ) ) = ( L ` ( G .+ E ) ) )
32	31	fveq2d	|- ( ph -> ( ._|_ ` ( L ` ( E .+ G ) ) ) = ( ._|_ ` ( L ` ( G .+ E ) ) ) )
33	32	fveq2d	|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( ._|_ ` ( ._|_ ` ( L ` ( G .+ E ) ) ) ) )
34	30 33 31	3eqtr4d	|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )