Theorem ressply1vsca

Description: A restricted power series algebra has the same scalar multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypotheses	ressply1.s	⊢ 𝑆 = ( Poly1 ‘ 𝑅 )
	ressply1.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	ressply1.u	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
	ressply1.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
	ressply1.2	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	ressply1.p	⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
Assertion	ressply1vsca	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		ressply1.s	⊢ 𝑆 = ( Poly1 ‘ 𝑅 )
2		ressply1.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
3		ressply1.u	⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
4		ressply1.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
5		ressply1.2	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6		ressply1.p	⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
7		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
8		eqid	⊢ ( 1o mPoly 𝐻 ) = ( 1o mPoly 𝐻 )
9		eqid	⊢ ( PwSer1 ‘ 𝐻 ) = ( PwSer1 ‘ 𝐻 )
10	3 9 4	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝐻 ) )
11		1on	⊢ 1o ∈ On
12	11	a1i	⊢ ( 𝜑 → 1o ∈ On )
13		eqid	⊢ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) = ( ( 1o mPoly 𝑅 ) ↾s 𝐵 )
14	7 2 8 10 12 5 13	ressmplvsca	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ ( 1o mPoly 𝐻 ) ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) ) 𝑌 ) )
15		eqid	⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
16	3 8 15	ply1vsca	⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ ( 1o mPoly 𝐻 ) )
17	16	oveqi	⊢ ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ ( 1o mPoly 𝐻 ) ) 𝑌 )
18		eqid	⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
19	1 7 18	ply1vsca	⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
20	4	fvexi	⊢ 𝐵 ∈ V
21	6 18	ressvsca	⊢ ( 𝐵 ∈ V → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑃 ) )
22	20 21	ax-mp	⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑃 )
23		eqid	⊢ ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
24	13 23	ressvsca	⊢ ( 𝐵 ∈ V → ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) = ( ·𝑠 ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) ) )
25	20 24	ax-mp	⊢ ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) = ( ·𝑠 ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) )
26	19 22 25	3eqtr3i	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) )
27	26	oveqi	⊢ ( 𝑋 ( ·𝑠 ‘ 𝑃 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) ) 𝑌 )
28	14 17 27	3eqtr4g	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( ·𝑠 ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) 𝑌 ) )