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 = ( LHyp ` K )
	hlhilsbase.l	|- L = ( ( DVecH ` K ) ` W )
	hlhilsbase.s	|- S = ( Scalar ` L )
	hlhilsbase.u	|- U = ( ( HLHil ` K ) ` W )
	hlhilsbase.r	|- R = ( Scalar ` U )
	hlhilsbase.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hlhils1.t	|- .1. = ( 1r ` S )
Assertion	hlhils1N	|- ( ph -> .1. = ( 1r ` R ) )

Proof

Step	Hyp	Ref	Expression
1		hlhilsbase.h	|- H = ( LHyp ` K )
2		hlhilsbase.l	|- L = ( ( DVecH ` K ) ` W )
3		hlhilsbase.s	|- S = ( Scalar ` L )
4		hlhilsbase.u	|- U = ( ( HLHil ` K ) ` W )
5		hlhilsbase.r	|- R = ( Scalar ` U )
6		hlhilsbase.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		hlhils1.t	|- .1. = ( 1r ` S )
8		eqidd	|- ( ph -> ( Base ` S ) = ( Base ` S ) )
9		eqid	|- ( Base ` S ) = ( Base ` S )
10	1 2 3 4 5 6 9	hlhilsbase2	|- ( ph -> ( Base ` S ) = ( Base ` R ) )
11		eqid	|- ( .r ` S ) = ( .r ` S )
12	1 2 3 4 5 6 11	hlhilsmul2	|- ( ph -> ( .r ` S ) = ( .r ` R ) )
13	12	oveqdr	|- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( x ( .r ` S ) y ) = ( x ( .r ` R ) y ) )
14	8 10 13	rngidpropd	|- ( ph -> ( 1r ` S ) = ( 1r ` R ) )
15	7 14	syl5eq	|- ( ph -> .1. = ( 1r ` R ) )