Metamath Proof Explorer


Theorem mplascl

Description: Value of the scalar injection into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015)

Ref Expression
Hypotheses mplascl.p P = I mPoly R
mplascl.d D = f 0 I | f -1 Fin
mplascl.z 0 ˙ = 0 R
mplascl.b B = Base R
mplascl.a A = algSc P
mplascl.i φ I W
mplascl.r φ R Ring
mplascl.x φ X B
Assertion mplascl φ A X = y D if y = I × 0 X 0 ˙

Proof

Step Hyp Ref Expression
1 mplascl.p P = I mPoly R
2 mplascl.d D = f 0 I | f -1 Fin
3 mplascl.z 0 ˙ = 0 R
4 mplascl.b B = Base R
5 mplascl.a A = algSc P
6 mplascl.i φ I W
7 mplascl.r φ R Ring
8 mplascl.x φ X B
9 1 6 7 mplsca φ R = Scalar P
10 9 fveq2d φ Base R = Base Scalar P
11 4 10 syl5eq φ B = Base Scalar P
12 8 11 eleqtrd φ X Base Scalar P
13 eqid Scalar P = Scalar P
14 eqid Base Scalar P = Base Scalar P
15 eqid P = P
16 eqid 1 P = 1 P
17 5 13 14 15 16 asclval X Base Scalar P A X = X P 1 P
18 12 17 syl φ A X = X P 1 P
19 eqid 1 R = 1 R
20 1 2 3 19 16 6 7 mpl1 φ 1 P = y D if y = I × 0 1 R 0 ˙
21 20 oveq2d φ X P 1 P = X P y D if y = I × 0 1 R 0 ˙
22 2 psrbag0 I W I × 0 D
23 6 22 syl φ I × 0 D
24 1 15 2 19 3 4 6 7 23 8 mplmon2 φ X P y D if y = I × 0 1 R 0 ˙ = y D if y = I × 0 X 0 ˙
25 18 21 24 3eqtrd φ A X = y D if y = I × 0 X 0 ˙