Theorem subrg1ascl

Description: The scalar injection function in a subring algebra is the same up to a restriction to the subring. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	subrg1ascl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	subrg1ascl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	subrg1ascl.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	subrg1ascl.u	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
	subrg1ascl.r	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	subrg1ascl.c	⊢ 𝐶 = ( algSc ‘ 𝑈 )
Assertion	subrg1ascl	⊢ ( 𝜑 → 𝐶 = ( 𝐴 ↾ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		subrg1ascl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		subrg1ascl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
3		subrg1ascl.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
4		subrg1ascl.u	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
5		subrg1ascl.r	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6		subrg1ascl.c	⊢ 𝐶 = ( algSc ‘ 𝑈 )
7		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
8	1 2	ply1ascl	⊢ 𝐴 = ( algSc ‘ ( 1o mPoly 𝑅 ) )
9		eqid	⊢ ( 1o mPoly 𝐻 ) = ( 1o mPoly 𝐻 )
10		1on	⊢ 1o ∈ On
11	10	a1i	⊢ ( 𝜑 → 1o ∈ On )
12	4 6	ply1ascl	⊢ 𝐶 = ( algSc ‘ ( 1o mPoly 𝐻 ) )
13	7 8 3 9 11 5 12	subrgascl	⊢ ( 𝜑 → 𝐶 = ( 𝐴 ↾ 𝑇 ) )