hlhilslemOLD

Description: Obsolete version of hlhilslem as of 6-Nov-2024. Lemma for hlhilsbase . (Contributed by Mario Carneiro, 28-Jun-2015) (New usage is discouraged.) (Proof modification is discouraged.)

	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 ) )
	hlhilslemOLD.f	\|- F = Slot N
	hlhilslemOLD.1	\|- N e. NN
	hlhilslemOLD.2	\|- N < 4
	hlhilslemOLD.c	\|- C = ( F ` E )
Assertion	hlhilslemOLD	\|- ( 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		hlhilslemOLD.f	\|- F = Slot N
7		hlhilslemOLD.1	\|- N e. NN
8		hlhilslemOLD.2	\|- N < 4
9		hlhilslemOLD.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	eqtrid	\|- ( ph -> C = ( F ` R ) )

Metamath Proof Explorer

Theorem hlhilslemOLD

Proof