Theorem hlhilslem

Description: Lemma for hlhilsbase2 . (Contributed by Mario Carneiro, 28-Jun-2015)

	Ref	Expression
Hypotheses	hlhilslem.h	|- H = ( LHyp ` K )
	hlhilslem.e	|- E = ( ( EDRing ` K ) ` W )
	hlhilslem.u	|- U = ( ( HLHil ` K ) ` W )
	hlhilslem.r	|- R = ( Scalar ` U )
	hlhilslem.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hlhilslem.f	|- F = Slot N
	hlhilslem.1	|- N e. NN
	hlhilslem.2	|- N < 4
	hlhilslem.c	|- C = ( F ` E )
Assertion	hlhilslem	|- ( ph -> C = ( F ` R ) )

Proof

Step	Hyp	Ref	Expression
1		hlhilslem.h	|- H = ( LHyp ` K )
2		hlhilslem.e	|- E = ( ( EDRing ` K ) ` W )
3		hlhilslem.u	|- U = ( ( HLHil ` K ) ` W )
4		hlhilslem.r	|- R = ( Scalar ` U )
5		hlhilslem.k	|- ( ph -> ( K e. HL /\ W e. H ) )
6		hlhilslem.f	|- F = Slot N
7		hlhilslem.1	|- N e. NN
8		hlhilslem.2	|- N < 4
9		hlhilslem.c	|- C = ( F ` E )
10	6 7	ndxid	|- F = Slot ( F ` ndx )
11	7	nnrei	|- N e. RR
12	11 8	ltneii	|- N =/= 4
13	6 7	ndxarg	|- ( F ` ndx ) = N
14		starvndx	|- ( *r ` ndx ) = 4
15	13 14	neeq12i	|- ( ( F ` ndx ) =/= ( *r ` ndx ) <-> N =/= 4 )
16	12 15	mpbir	|- ( F ` ndx ) =/= ( *r ` ndx )
17	10 16	setsnid	|- ( F ` E ) = ( F ` ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) )
18	9 17	eqtri	|- C = ( F ` ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) )
19		eqid	|- ( ( HGMap ` K ) ` W ) = ( ( HGMap ` K ) ` W )
20		eqid	|- ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) = ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. )
21	1 3 5 2 19 20	hlhilsca	|- ( ph -> ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) = ( Scalar ` U ) )
22	21 4	eqtr4di	|- ( ph -> ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) = R )
23	22	fveq2d	|- ( ph -> ( F ` ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) ) = ( F ` R ) )
24	18 23	syl5eq	|- ( ph -> C = ( F ` R ) )