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

Metamath Proof Explorer

Theorem mplmon2cl

Description: A scaled monomial is a polynomial. (Contributed by Stefan O'Rear, 8-Mar-2015)

Ref Expression
Hypotheses mplmon2cl.p ⊢ P = I mPoly R
mplmon2cl.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
mplmon2cl.z ⊢ 0 ˙ = 0 R
mplmon2cl.c ⊢ C = Base R
mplmon2cl.i ⊢ φ → I ∈ W
mplmon2cl.r ⊢ φ → R ∈ Ring
mplmon2cl.b ⊢ B = Base P
mplmon2cl.x ⊢ φ → X ∈ C
mplmon2cl.k ⊢ φ → K ∈ D
Assertion mplmon2cl ⊢ φ → y ∈ D ⟼ if y = K X 0 ˙ ∈ B

Proof

Step Hyp Ref Expression
1 mplmon2cl.p ⊢ P = I mPoly R
2 mplmon2cl.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
3 mplmon2cl.z ⊢ 0 ˙ = 0 R
4 mplmon2cl.c ⊢ C = Base R
5 mplmon2cl.i ⊢ φ → I ∈ W
6 mplmon2cl.r ⊢ φ → R ∈ Ring
7 mplmon2cl.b ⊢ B = Base P
8 mplmon2cl.x ⊢ φ → X ∈ C
9 mplmon2cl.k ⊢ φ → K ∈ D
10 eqid ⊢ ⋅ P = ⋅ P
11 eqid ⊢ 1 R = 1 R
12 1 10 2 11 3 4 5 6 9 8 mplmon2 ⊢ φ → X ⋅ P y ∈ D ⟼ if y = K 1 R 0 ˙ = y ∈ D ⟼ if y = K X 0 ˙
13 1 5 6 mpllmodd ⊢ φ → P ∈ LMod
14 1 5 6 mplsca ⊢ φ → R = Scalar ⁡ P
15 14 fveq2d ⊢ φ → Base R = Base Scalar ⁡ P
16 4 15 eqtrid ⊢ φ → C = Base Scalar ⁡ P
17 8 16 eleqtrd ⊢ φ → X ∈ Base Scalar ⁡ P
18 1 7 3 11 2 5 6 9 mplmon ⊢ φ → y ∈ D ⟼ if y = K 1 R 0 ˙ ∈ B
19 eqid ⊢ Scalar ⁡ P = Scalar ⁡ P
20 eqid ⊢ Base Scalar ⁡ P = Base Scalar ⁡ P
21 7 19 10 20 lmodvscl ⊢ P ∈ LMod ∧ X ∈ Base Scalar ⁡ P ∧ y ∈ D ⟼ if y = K 1 R 0 ˙ ∈ B → X ⋅ P y ∈ D ⟼ if y = K 1 R 0 ˙ ∈ B
22 13 17 18 21 syl3anc ⊢ φ → X ⋅ P y ∈ D ⟼ if y = K 1 R 0 ˙ ∈ B
23 12 22 eqeltrrd ⊢ φ → y ∈ D ⟼ if y = K X 0 ˙ ∈ B