Theorem hlhils1N

Description: The scalar ring unity for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 29-Jun-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hlhilsbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hlhilsbase.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hlhilsbase.s	$$⊢S=\mathrm{Scalar}\left(L\right)$$
	hlhilsbase.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhilsbase.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hlhilsbase.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hlhils1.t	$$⊢\underset{\dot{}}{1}=1_S$$
Assertion	hlhils1N	$$⊢\phi \to \underset{\dot{}}{1}=1_R$$

Proof

Step	Hyp	Ref	Expression
1		hlhilsbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhilsbase.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hlhilsbase.s	$$⊢S=\mathrm{Scalar}\left(L\right)$$
4		hlhilsbase.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
5		hlhilsbase.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hlhilsbase.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		hlhils1.t	$$⊢\underset{\dot{}}{1}=1_S$$
8		eqidd	$$⊢\phi \to {\mathrm{Base}}_S={\mathrm{Base}}_S$$
9		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
10	1 2 3 4 5 6 9	hlhilsbase2	$$⊢\phi \to {\mathrm{Base}}_S={\mathrm{Base}}_R$$
11		eqid	$$⊢{\cdot }_S={\cdot }_S$$
12	1 2 3 4 5 6 11	hlhilsmul2	$$⊢\phi \to {\cdot }_S={\cdot }_R$$
13	12	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\right)\to x{\cdot }_{S}y=x{\cdot }_{R}y$$
14	8 10 13	rngidpropd	$$⊢\phi \to 1_S=1_R$$
15	7 14	syl5eq	$$⊢\phi \to \underset{\dot{}}{1}=1_R$$