Theorem sra1r

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

	Ref	Expression
Hypotheses	sral1r.a	$$⊢\phi \to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
	sral1r.1	$$⊢\phi \to \underset{\dot{}}{1}=1_W$$
	sral1r.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
Assertion	sra1r	$$⊢\phi \to \underset{\dot{}}{1}=1_A$$

Proof

Step	Hyp	Ref	Expression
1		sral1r.a	$$⊢\phi \to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
2		sral1r.1	$$⊢\phi \to \underset{\dot{}}{1}=1_W$$
3		sral1r.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
4		eqidd	$$⊢\phi \to {\mathrm{Base}}_W={\mathrm{Base}}_W$$
5	1 3	srabase	$$⊢\phi \to {\mathrm{Base}}_W={\mathrm{Base}}_A$$
6	1 3	sramulr	$$⊢\phi \to {\cdot }_W={\cdot }_A$$
7	6	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_W\wedge y\in {\mathrm{Base}}_W\right)\right)\to x{\cdot }_{W}y=x{\cdot }_{A}y$$
8	4 5 7	rngidpropd	$$⊢\phi \to 1_W=1_A$$
9	2 8	eqtrd	$$⊢\phi \to \underset{\dot{}}{1}=1_A$$