Theorem 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=\mathrm{LHyp}\left(K\right)$$
	hlhilslem.e	$$⊢E=\mathrm{EDRing}\left(K\right)\left(W\right)$$
	hlhilslem.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhilslem.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hlhilslem.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hlhilslemOLD.f	$$⊢F=\mathrm{Slot}N$$
	hlhilslemOLD.1	$$⊢N\in \mathbb{N}$$
	hlhilslemOLD.2	$$⊢N<4$$
	hlhilslemOLD.c	$$⊢C=F\left(E\right)$$
Assertion	hlhilslemOLD	$$⊢\phi \to C=F\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlhilslem.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhilslem.e	$$⊢E=\mathrm{EDRing}\left(K\right)\left(W\right)$$
3		hlhilslem.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
4		hlhilslem.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
5		hlhilslem.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6		hlhilslemOLD.f	$$⊢F=\mathrm{Slot}N$$
7		hlhilslemOLD.1	$$⊢N\in \mathbb{N}$$
8		hlhilslemOLD.2	$$⊢N<4$$
9		hlhilslemOLD.c	$$⊢C=F\left(E\right)$$
10	6 7	ndxid	$$⊢F=\mathrm{Slot}F\left(\mathrm{ndx}\right)$$
11	7	nnrei	$$⊢N\in ℝ$$
12	11 8	ltneii	$$⊢N\ne 4$$
13	6 7	ndxarg	$$⊢F\left(\mathrm{ndx}\right)=N$$
14		starvndx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}=4$$
15	13 14	neeq12i	$$⊢F\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}\leftrightarrow N\ne 4$$
16	12 15	mpbir	$$⊢F\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
17	10 16	setsnid	$$⊢F\left(E\right)=F\left(E\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩\right)$$
18	9 17	eqtri	$$⊢C=F\left(E\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩\right)$$
19		eqid	$$⊢\mathrm{HGMap}\left(K\right)\left(W\right)=\mathrm{HGMap}\left(K\right)\left(W\right)$$
20		eqid	$$⊢E\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩=E\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩$$
21	1 3 5 2 19 20	hlhilsca	$$⊢\phi \to E\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩=\mathrm{Scalar}\left(U\right)$$
22	21 4	eqtr4di	$$⊢\phi \to E\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩=R$$
23	22	fveq2d	$$⊢\phi \to F\left(E\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩\right)=F\left(R\right)$$
24	18 23	syl5eq	$$⊢\phi \to C=F\left(R\right)$$