Metamath Proof Explorer

Theorem ressply1mul

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

Ref Expression
Hypotheses ressply1.s ⊢ S = Poly 1 ⁡ R
ressply1.h ⊢ H = R ↾ 𝑠 T
ressply1.u ⊢ U = Poly 1 ⁡ H
ressply1.b ⊢ B = Base U
ressply1.2 ⊢ φ → T ∈ SubRing ⁡ R
ressply1.p ⊢ P = S ↾ 𝑠 B
Assertion ressply1mul ⊢ φ ∧ X ∈ B ∧ Y ∈ B → X ⋅ U Y = X ⋅ P Y

Proof

Step Hyp Ref Expression
1 ressply1.s ⊢ S = Poly 1 ⁡ R
2 ressply1.h ⊢ H = R ↾ 𝑠 T
3 ressply1.u ⊢ U = Poly 1 ⁡ H
4 ressply1.b ⊢ B = Base U
5 ressply1.2 ⊢ φ → T ∈ SubRing ⁡ R
6 ressply1.p ⊢ P = S ↾ 𝑠 B
7 eqid ⊢ 1 𝑜 mPoly R = 1 𝑜 mPoly R
8 eqid ⊢ 1 𝑜 mPoly H = 1 𝑜 mPoly H
9 3 4 ply1bas ⊢ B = Base 1 𝑜 mPoly H
10 1on ⊢ 1 𝑜 ∈ On
11 10 a1i ⊢ φ → 1 𝑜 ∈ On
12 eqid ⊢ 1 𝑜 mPoly R ↾ 𝑠 B = 1 𝑜 mPoly R ↾ 𝑠 B
13 7 2 8 9 11 5 12 ressmplmul ⊢ φ ∧ X ∈ B ∧ Y ∈ B → X ⋅ 1 𝑜 mPoly H Y = X ⋅ 1 𝑜 mPoly R ↾ 𝑠 B Y
14 eqid ⊢ ⋅ U = ⋅ U
15 3 8 14 ply1mulr ⊢ ⋅ U = ⋅ 1 𝑜 mPoly H
16 15 oveqi ⊢ X ⋅ U Y = X ⋅ 1 𝑜 mPoly H Y
17 eqid ⊢ ⋅ S = ⋅ S
18 1 7 17 ply1mulr ⊢ ⋅ S = ⋅ 1 𝑜 mPoly R
19 4 fvexi ⊢ B ∈ V
20 6 17 ressmulr ⊢ B ∈ V → ⋅ S = ⋅ P
21 19 20 ax-mp ⊢ ⋅ S = ⋅ P
22 eqid ⊢ ⋅ 1 𝑜 mPoly R = ⋅ 1 𝑜 mPoly R
23 12 22 ressmulr ⊢ B ∈ V → ⋅ 1 𝑜 mPoly R = ⋅ 1 𝑜 mPoly R ↾ 𝑠 B
24 19 23 ax-mp ⊢ ⋅ 1 𝑜 mPoly R = ⋅ 1 𝑜 mPoly R ↾ 𝑠 B
25 18 21 24 3eqtr3i ⊢ ⋅ P = ⋅ 1 𝑜 mPoly R ↾ 𝑠 B
26 25 oveqi ⊢ X ⋅ P Y = X ⋅ 1 𝑜 mPoly R ↾ 𝑠 B Y
27 13 16 26 3eqtr4g ⊢ φ ∧ X ∈ B ∧ Y ∈ B → X ⋅ U Y = X ⋅ P Y