Theorem sra1r

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

	Ref	Expression
Hypotheses	sral1r.a	⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
	sral1r.1	⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑊 ) )
	sral1r.s	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
Assertion	sra1r	⊢ ( 𝜑 → 1 = ( 1r ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		sral1r.a	⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
2		sral1r.1	⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑊 ) )
3		sral1r.s	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
4		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
5	1 3	srabase	⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ 𝐴 ) )
6	1 3	sramulr	⊢ ( 𝜑 → ( .r ‘ 𝑊 ) = ( .r ‘ 𝐴 ) )
7	6	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) )
8	4 5 7	rngidpropd	⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝐴 ) )
9	2 8	eqtrd	⊢ ( 𝜑 → 1 = ( 1r ‘ 𝐴 ) )