lclkrlem2i

Description: Lemma for lclkr . Eliminate the ( LE ) =/= ( LG ) hypothesis. (Contributed by NM, 17-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 } ) ) )
	lclkrlem2i.x	\|- ( ph -> X e. ( V \ { .0. } ) )
	lclkrlem2i.y	\|- ( ph -> Y e. ( V \ { .0. } ) )
Assertion	lclkrlem2i	\|- ( 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		lclkrlem2i.x	\|- ( ph -> X e. ( V \ { .0. } ) )
24		lclkrlem2i.y	\|- ( ph -> Y e. ( V \ { .0. } ) )
25	15	adantr	\|- ( ( ph /\ ( L ` E ) = ( L ` G ) ) -> ( K e. HL /\ W e. H ) )
26	23	adantr	\|- ( ( ph /\ ( L ` E ) = ( L ` G ) ) -> X e. ( V \ { .0. } ) )
27	17	adantr	\|- ( ( ph /\ ( L ` E ) = ( L ` G ) ) -> E e. F )
28	18	adantr	\|- ( ( ph /\ ( L ` E ) = ( L ` G ) ) -> G e. F )
29	19	adantr	\|- ( ( ph /\ ( L ` E ) = ( L ` G ) ) -> ( L ` E ) = ( ._\|_ ` { X } ) )
30		simpr	\|- ( ( ph /\ ( L ` E ) = ( L ` G ) ) -> ( L ` E ) = ( L ` G ) )
31	1 2 3 4 7 10 12 13 14 25 26 27 28 29 30	lclkrlem2e	\|- ( ( ph /\ ( L ` E ) = ( L ` G ) ) -> ( ._\|_ ` ( ._\|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
32	15	adantr	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> ( K e. HL /\ W e. H ) )
33	16	adantr	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> B e. ( V \ { .0. } ) )
34	17	adantr	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> E e. F )
35	18	adantr	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> G e. F )
36	19	adantr	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> ( L ` E ) = ( ._\|_ ` { X } ) )
37	20	adantr	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> ( L ` G ) = ( ._\|_ ` { Y } ) )
38	21	adantr	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> ( ( E .+ G ) ` B ) = Q )
39	22	adantr	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> ( -. X e. ( ._\|_ ` { B } ) \/ -. Y e. ( ._\|_ ` { B } ) ) )
40	23	adantr	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> X e. ( V \ { .0. } ) )
41	24	adantr	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> Y e. ( V \ { .0. } ) )
42		simpr	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> ( L ` E ) =/= ( L ` G ) )
43	1 2 3 4 5 6 7 8 9 10 11 12 13 14 32 33 34 35 36 37 38 39 40 41 42	lclkrlem2h	\|- ( ( ph /\ ( L ` E ) =/= ( L ` G ) ) -> ( ._\|_ ` ( ._\|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
44	31 43	pm2.61dane	\|- ( ph -> ( ._\|_ ` ( ._\|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )

Metamath Proof Explorer

Theorem lclkrlem2i

Proof