Theorem hlhilslem

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

	Ref	Expression
Hypotheses	hlhilslem.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hlhilslem.e	⊢ 𝐸 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
	hlhilslem.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
	hlhilslem.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hlhilslem.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hlhilslem.f	⊢ 𝐹 = Slot 𝑁
	hlhilslem.1	⊢ 𝑁 ∈ ℕ
	hlhilslem.2	⊢ 𝑁 < 4
	hlhilslem.c	⊢ 𝐶 = ( 𝐹 ‘ 𝐸 )
Assertion	hlhilslem	⊢ ( 𝜑 → 𝐶 = ( 𝐹 ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		hlhilslem.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hlhilslem.e	⊢ 𝐸 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
3		hlhilslem.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
4		hlhilslem.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
5		hlhilslem.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		hlhilslem.f	⊢ 𝐹 = Slot 𝑁
7		hlhilslem.1	⊢ 𝑁 ∈ ℕ
8		hlhilslem.2	⊢ 𝑁 < 4
9		hlhilslem.c	⊢ 𝐶 = ( 𝐹 ‘ 𝐸 )
10	6 7	ndxid	⊢ 𝐹 = Slot ( 𝐹 ‘ ndx )
11	7	nnrei	⊢ 𝑁 ∈ ℝ
12	11 8	ltneii	⊢ 𝑁 ≠ 4
13	6 7	ndxarg	⊢ ( 𝐹 ‘ ndx ) = 𝑁
14		starvndx	⊢ ( *𝑟 ‘ ndx ) = 4
15	13 14	neeq12i	⊢ ( ( 𝐹 ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ↔ 𝑁 ≠ 4 )
16	12 15	mpbir	⊢ ( 𝐹 ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
17	10 16	setsnid	⊢ ( 𝐹 ‘ 𝐸 ) = ( 𝐹 ‘ ( 𝐸 sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) )
18	9 17	eqtri	⊢ 𝐶 = ( 𝐹 ‘ ( 𝐸 sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) )
19		eqid	⊢ ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
20		eqid	⊢ ( 𝐸 sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) = ( 𝐸 sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ )
21	1 3 5 2 19 20	hlhilsca	⊢ ( 𝜑 → ( 𝐸 sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) = ( Scalar ‘ 𝑈 ) )
22	21 4	eqtr4di	⊢ ( 𝜑 → ( 𝐸 sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) = 𝑅 )
23	22	fveq2d	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐸 sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) ⟩ ) ) = ( 𝐹 ‘ 𝑅 ) )
24	18 23	syl5eq	⊢ ( 𝜑 → 𝐶 = ( 𝐹 ‘ 𝑅 ) )