Theorem hlhilnvl

Description: The involution operation of the star division ring for the final constructed Hilbert space. (Contributed by NM, 20-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

	Ref	Expression
Hypotheses	hlhilnvl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hlhilnvl.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
	hlhilnvl.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hlhilnvl.i	⊢ ∗ = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
	hlhilnvl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	hlhilnvl	⊢ ( 𝜑 → ∗ = ( *𝑟 ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		hlhilnvl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hlhilnvl.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
3		hlhilnvl.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
4		hlhilnvl.i	⊢ ∗ = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
5		hlhilnvl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		fvex	⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
7	4	fvexi	⊢ ∗ ∈ V
8		starvid	⊢ *𝑟 = Slot ( *𝑟 ‘ ndx )
9	8	setsid	⊢ ( ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ V ∧ ∗ ∈ V ) → ∗ = ( *𝑟 ‘ ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ ) ) )
10	6 7 9	mp2an	⊢ ∗ = ( *𝑟 ‘ ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ ) )
11		eqid	⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
12		eqid	⊢ ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ ) = ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ )
13	1 2 5 11 4 12	hlhilsca	⊢ ( 𝜑 → ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ ) = ( Scalar ‘ 𝑈 ) )
14	13 3	eqtr4di	⊢ ( 𝜑 → ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ ) = 𝑅 )
15	14	fveq2d	⊢ ( 𝜑 → ( *𝑟 ‘ ( ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ ) ) = ( *𝑟 ‘ 𝑅 ) )
16	10 15	syl5eq	⊢ ( 𝜑 → ∗ = ( *𝑟 ‘ 𝑅 ) )