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	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hlhilnvl.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhilnvl.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hlhilnvl.i	$$⊢\underset{\dot{}}{\ast }=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hlhilnvl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	hlhilnvl	$$⊢\phi \to \underset{\dot{}}{\ast }={\mathrm{*}}_R$$

Proof

Step	Hyp	Ref	Expression
1		hlhilnvl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhilnvl.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
3		hlhilnvl.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
4		hlhilnvl.i	$$⊢\underset{\dot{}}{\ast }=\mathrm{HGMap}\left(K\right)\left(W\right)$$
5		hlhilnvl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6		fvex	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)\in \mathrm{V}$$
7	4	fvexi	$$⊢\underset{\dot{}}{\ast }\in \mathrm{V}$$
8		starvid	$$⊢{\ast }_{𝑟}=\mathrm{Slot}{\mathrm{*}}_{\mathrm{ndx}}$$
9	8	setsid	$$⊢\left(\mathrm{EDRing}\left(K\right)\left(W\right)\in \mathrm{V}\wedge \underset{\dot{}}{\ast }\in \mathrm{V}\right)\to \underset{\dot{}}{\ast }={\mathrm{*}}_{\left(\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\underset{\dot{}}{\ast }⟩\right)}$$
10	6 7 9	mp2an	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_{\left(\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\underset{\dot{}}{\ast }⟩\right)}$$
11		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
12		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\underset{\dot{}}{\ast }⟩=\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\underset{\dot{}}{\ast }⟩$$
13	1 2 5 11 4 12	hlhilsca	$$⊢\phi \to \mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\underset{\dot{}}{\ast }⟩=\mathrm{Scalar}\left(U\right)$$
14	13 3	eqtr4di	$$⊢\phi \to \mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\underset{\dot{}}{\ast }⟩=R$$
15	14	fveq2d	$$⊢\phi \to {\mathrm{*}}_{\left(\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\underset{\dot{}}{\ast }⟩\right)}={\mathrm{*}}_R$$
16	10 15	syl5eq	$$⊢\phi \to \underset{\dot{}}{\ast }={\mathrm{*}}_R$$