Metamath Proof Explorer

Theorem ressmpladd

Description: A restricted polynomial algebra has the same addition 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 ressmpladd ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑃 ) 𝑌 ) )

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 resspsradd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∧ 𝑌 ∈ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) → ( 𝑋 ( +g ‘ ( 𝐼 mPwSer 𝐻 ) ) 𝑌 ) = ( 𝑋 ( +g ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) 𝑌 ) )
17 13 16 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ ( 𝐼 mPwSer 𝐻 ) ) 𝑌 ) = ( 𝑋 ( +g ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) 𝑌 ) )
18 4 fvexi ⊢ 𝐵 ∈ V
19 3 8 4 mplval2 ⊢ 𝑈 = ( ( 𝐼 mPwSer 𝐻 ) ↾s 𝐵 )
20 eqid ⊢ ( +g ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( +g ‘ ( 𝐼 mPwSer 𝐻 ) )
21 19 20 ressplusg ⊢ ( 𝐵 ∈ V → ( +g ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( +g ‘ 𝑈 ) )
22 18 21 ax-mp ⊢ ( +g ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( +g ‘ 𝑈 )
23 22 oveqi ⊢ ( 𝑋 ( +g ‘ ( 𝐼 mPwSer 𝐻 ) ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑈 ) 𝑌 )
24 fvex ⊢ ( Base ‘ 𝑆 ) ∈ V
25 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
26 1 14 25 mplval2 ⊢ 𝑆 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑆 ) )
27 eqid ⊢ ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ ( 𝐼 mPwSer 𝑅 ) )
28 26 27 ressplusg ⊢ ( ( Base ‘ 𝑆 ) ∈ V → ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ 𝑆 ) )
29 24 28 ax-mp ⊢ ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ 𝑆 )
30 fvex ⊢ ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∈ V
31 15 27 ressplusg ⊢ ( ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∈ V → ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) )
32 30 31 ax-mp ⊢ ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) )
33 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
34 7 33 ressplusg ⊢ ( 𝐵 ∈ V → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑃 ) )
35 18 34 ax-mp ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑃 )
36 29 32 35 3eqtr3i ⊢ ( +g ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) = ( +g ‘ 𝑃 )
37 36 oveqi ⊢ ( 𝑋 ( +g ‘ ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ) ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑃 ) 𝑌 )
38 17 23 37 3eqtr3g ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑃 ) 𝑌 ) )