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

Metamath Proof Explorer

Theorem ressply1add

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

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 3 4 ply1bas ⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝐻 ) )
10 1on ⊢ 1o ∈ On
11 10 a1i ⊢ ( 𝜑 → 1o ∈ On )
12 eqid ⊢ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) = ( ( 1o mPoly 𝑅 ) ↾s 𝐵 )
13 7 2 8 9 11 5 12 ressmpladd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ ( 1o mPoly 𝐻 ) ) 𝑌 ) = ( 𝑋 ( +g ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) ) 𝑌 ) )
14 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
15 3 8 14 ply1plusg ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ ( 1o mPoly 𝐻 ) )
16 15 oveqi ⊢ ( 𝑋 ( +g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( +g ‘ ( 1o mPoly 𝐻 ) ) 𝑌 )
17 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
18 1 7 17 ply1plusg ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ ( 1o mPoly 𝑅 ) )
19 4 fvexi ⊢ 𝐵 ∈ V
20 6 17 ressplusg ⊢ ( 𝐵 ∈ V → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑃 ) )
21 19 20 ax-mp ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑃 )
22 eqid ⊢ ( +g ‘ ( 1o mPoly 𝑅 ) ) = ( +g ‘ ( 1o mPoly 𝑅 ) )
23 12 22 ressplusg ⊢ ( 𝐵 ∈ V → ( +g ‘ ( 1o mPoly 𝑅 ) ) = ( +g ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) ) )
24 19 23 ax-mp ⊢ ( +g ‘ ( 1o mPoly 𝑅 ) ) = ( +g ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) )
25 18 21 24 3eqtr3i ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) )
26 25 oveqi ⊢ ( 𝑋 ( +g ‘ 𝑃 ) 𝑌 ) = ( 𝑋 ( +g ‘ ( ( 1o mPoly 𝑅 ) ↾s 𝐵 ) ) 𝑌 )
27 13 16 26 3eqtr4g ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( +g ‘ 𝑈 ) 𝑌 ) = ( 𝑋 ( +g ‘ 𝑃 ) 𝑌 ) )