Theorem hlhilslem

Description: Lemma for hlhilsbase etc. (Contributed by Mario Carneiro, 28-Jun-2015) (Revised by AV, 6-Nov-2024)

	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 ( F ` ndx )
	hlhilslem.n	|- ( F ` ndx ) =/= ( *r ` ndx )
	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 ( F ` ndx )
7		hlhilslem.n	|- ( F ` ndx ) =/= ( *r ` ndx )
8		hlhilslem.c	|- C = ( F ` E )
9	6 7	setsnid	|- ( F ` E ) = ( F ` ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) )
10	8 9	eqtri	|- C = ( F ` ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) )
11		eqid	|- ( ( HGMap ` K ) ` W ) = ( ( HGMap ` K ) ` W )
12		eqid	|- ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) = ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. )
13	1 3 5 2 11 12	hlhilsca	|- ( ph -> ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) = ( Scalar ` U ) )
14	13 4	eqtr4di	|- ( ph -> ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) = R )
15	14	fveq2d	|- ( ph -> ( F ` ( E sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) ) = ( F ` R ) )
16	10 15	syl5eq	|- ( ph -> C = ( F ` R ) )