This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐶 = ( 𝐴 ↾ 𝑇 ) )