Theorem ressmplmul

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

	Ref	Expression
Hypotheses	ressmpl.s	⊢ 𝑆 = ( 𝐼 mPoly 𝑅 )
	ressmpl.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	ressmpl.u	⊢ 𝑈 = ( 𝐼 mPoly 𝐻 )
	ressmpl.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
	ressmpl.1	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	ressmpl.2	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	ressmpl.p	⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
Assertion	ressmplmul	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( .r ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( .r ‘ 𝑃 ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		ressmpl.s	⊢ 𝑆 = ( 𝐼 mPoly 𝑅 )
2		ressmpl.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
3		ressmpl.u	⊢ 𝑈 = ( 𝐼 mPoly 𝐻 )
4		ressmpl.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
5		ressmpl.1	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		ressmpl.2	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
7		ressmpl.p	⊢ 𝑃 = ( 𝑆 ↾s 𝐵 )
8		eqid	⊢ ( 𝐼 mPwSer 𝐻 ) = ( 𝐼 mPwSer 𝐻 )
9		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝐻 ) )
10	3 8 4 9	mplbasss	⊢ 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) )
11	10	sseli	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) )
12	10	sseli	⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) )
13	11 12	anim12i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∧ 𝑌 ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) )
14		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
15		eqid	⊢ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) )
16	14 2 8 9 15 6	resspsrmul	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∧ 𝑌 ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) → ( 𝑋 ( .r ‘ ( 𝐼 mPwSer 𝐻 ) ) 𝑌 ) = ( 𝑋 ( .r ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) 𝑌 ) )
17	13 16	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( .r ‘ ( 𝐼 mPwSer 𝐻 ) ) 𝑌 ) = ( 𝑋 ( .r ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) 𝑌 ) )
18	4	fvexi	⊢ 𝐵 ∈ V
19	3 8 4	mplval2	⊢ 𝑈 = ( ( 𝐼 mPwSer 𝐻 ) ↾s 𝐵 )
20		eqid	⊢ ( .r ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( .r ‘ ( 𝐼 mPwSer 𝐻 ) )
21	19 20	ressmulr	⊢ ( 𝐵 ∈ V → ( .r ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( .r ‘ 𝑈 ) )
22	18 21	ax-mp	⊢ ( .r ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( .r ‘ 𝑈 )
23	22	oveqi	⊢ ( 𝑋 ( .r ‘ ( 𝐼 mPwSer 𝐻 ) ) 𝑌 ) = ( 𝑋 ( .r ‘ 𝑈 ) 𝑌 )
24		fvex	⊢ ( Base ‘ 𝑆 ) ∈ V
25		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
26	1 14 25	mplval2	⊢ 𝑆 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑆 ) )
27		eqid	⊢ ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( .r ‘ ( 𝐼 mPwSer 𝑅 ) )
28	26 27	ressmulr	⊢ ( ( Base ‘ 𝑆 ) ∈ V → ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( .r ‘ 𝑆 ) )
29	24 28	ax-mp	⊢ ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( .r ‘ 𝑆 )
30		fvex	⊢ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∈ V
31	15 27	ressmulr	⊢ ( ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∈ V → ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( .r ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) )
32	30 31	ax-mp	⊢ ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( .r ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) )
33		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
34	7 33	ressmulr	⊢ ( 𝐵 ∈ V → ( .r ‘ 𝑆 ) = ( .r ‘ 𝑃 ) )
35	18 34	ax-mp	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑃 )
36	29 32 35	3eqtr3i	⊢ ( .r ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) = ( .r ‘ 𝑃 )
37	36	oveqi	⊢ ( 𝑋 ( .r ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) 𝑌 ) = ( 𝑋 ( .r ‘ 𝑃 ) 𝑌 )
38	17 23 37	3eqtr3g	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( .r ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( .r ‘ 𝑃 ) 𝑌 ) )