Theorem lcfrlem24

Description: Lemma for lcfr . (Contributed by NM, 24-Feb-2015)

	Ref	Expression
Hypotheses	lcfrlem17.h	|- H = ( LHyp ` K )
	lcfrlem17.o	|- ._|_ = ( ( ocH ` K ) ` W )
	lcfrlem17.u	|- U = ( ( DVecH ` K ) ` W )
	lcfrlem17.v	|- V = ( Base ` U )
	lcfrlem17.p	|- .+ = ( +g ` U )
	lcfrlem17.z	|- .0. = ( 0g ` U )
	lcfrlem17.n	|- N = ( LSpan ` U )
	lcfrlem17.a	|- A = ( LSAtoms ` U )
	lcfrlem17.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcfrlem17.x	|- ( ph -> X e. ( V \ { .0. } ) )
	lcfrlem17.y	|- ( ph -> Y e. ( V \ { .0. } ) )
	lcfrlem17.ne	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
	lcfrlem22.b	|- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )
	lcfrlem24.t	|- .x. = ( .s ` U )
	lcfrlem24.s	|- S = ( Scalar ` U )
	lcfrlem24.q	|- Q = ( 0g ` S )
	lcfrlem24.r	|- R = ( Base ` S )
	lcfrlem24.j	|- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
	lcfrlem24.ib	|- ( ph -> I e. B )
	lcfrlem24.l	|- L = ( LKer ` U )
Assertion	lcfrlem24	|- ( ph -> ( ._|_ ` { X , Y } ) = ( ( L ` ( J ` X ) ) i^i ( L ` ( J ` Y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcfrlem17.h	|- H = ( LHyp ` K )
2		lcfrlem17.o	|- ._|_ = ( ( ocH ` K ) ` W )
3		lcfrlem17.u	|- U = ( ( DVecH ` K ) ` W )
4		lcfrlem17.v	|- V = ( Base ` U )
5		lcfrlem17.p	|- .+ = ( +g ` U )
6		lcfrlem17.z	|- .0. = ( 0g ` U )
7		lcfrlem17.n	|- N = ( LSpan ` U )
8		lcfrlem17.a	|- A = ( LSAtoms ` U )
9		lcfrlem17.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		lcfrlem17.x	|- ( ph -> X e. ( V \ { .0. } ) )
11		lcfrlem17.y	|- ( ph -> Y e. ( V \ { .0. } ) )
12		lcfrlem17.ne	|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
13		lcfrlem22.b	|- B = ( ( N ` { X , Y } ) i^i ( ._|_ ` { ( X .+ Y ) } ) )
14		lcfrlem24.t	|- .x. = ( .s ` U )
15		lcfrlem24.s	|- S = ( Scalar ` U )
16		lcfrlem24.q	|- Q = ( 0g ` S )
17		lcfrlem24.r	|- R = ( Base ` S )
18		lcfrlem24.j	|- J = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ k e. R E. w e. ( ._|_ ` { x } ) v = ( w .+ ( k .x. x ) ) ) ) )
19		lcfrlem24.ib	|- ( ph -> I e. B )
20		lcfrlem24.l	|- L = ( LKer ` U )
21	1 2 3 4 5 6 7 8 9 10 11 12	lcfrlem18	|- ( ph -> ( ._|_ ` { X , Y } ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
22		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
23		eqid	|- ( LDual ` U ) = ( LDual ` U )
24		eqid	|- ( 0g ` ( LDual ` U ) ) = ( 0g ` ( LDual ` U ) )
25		eqid	|- { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) } = { f e. ( LFnl ` U ) | ( ._|_ ` ( ._|_ ` ( L ` f ) ) ) = ( L ` f ) }
26	1 2 3 4 5 14 15 17 6 22 20 23 24 25 18 9 10	lcfrlem11	|- ( ph -> ( L ` ( J ` X ) ) = ( ._|_ ` { X } ) )
27	1 2 3 4 5 14 15 17 6 22 20 23 24 25 18 9 11	lcfrlem11	|- ( ph -> ( L ` ( J ` Y ) ) = ( ._|_ ` { Y } ) )
28	26 27	ineq12d	|- ( ph -> ( ( L ` ( J ` X ) ) i^i ( L ` ( J ` Y ) ) ) = ( ( ._|_ ` { X } ) i^i ( ._|_ ` { Y } ) ) )
29	21 28	eqtr4d	|- ( ph -> ( ._|_ ` { X , Y } ) = ( ( L ` ( J ` X ) ) i^i ( L ` ( J ` Y ) ) ) )