Theorem sra1r

Description: The multiplicative neutral element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023)

	Ref	Expression
Hypotheses	sral1r.a	|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
	sral1r.1	|- ( ph -> .1. = ( 1r ` W ) )
	sral1r.s	|- ( ph -> S C_ ( Base ` W ) )
Assertion	sra1r	|- ( ph -> .1. = ( 1r ` A ) )

Proof

Step	Hyp	Ref	Expression
1		sral1r.a	|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
2		sral1r.1	|- ( ph -> .1. = ( 1r ` W ) )
3		sral1r.s	|- ( ph -> S C_ ( Base ` W ) )
4		eqidd	|- ( ph -> ( Base ` W ) = ( Base ` W ) )
5	1 3	srabase	|- ( ph -> ( Base ` W ) = ( Base ` A ) )
6	1 3	sramulr	|- ( ph -> ( .r ` W ) = ( .r ` A ) )
7	6	oveqdr	|- ( ( ph /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( .r ` W ) y ) = ( x ( .r ` A ) y ) )
8	4 5 7	rngidpropd	|- ( ph -> ( 1r ` W ) = ( 1r ` A ) )
9	2 8	eqtrd	|- ( ph -> .1. = ( 1r ` A ) )