Metamath Proof Explorer


Theorem mplmon2

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

Ref Expression
Hypotheses mplmon2.p P=ImPolyR
mplmon2.v ·˙=P
mplmon2.d D=f0I|f-1Fin
mplmon2.o 1˙=1R
mplmon2.z 0˙=0R
mplmon2.b B=BaseR
mplmon2.i φIW
mplmon2.r φRRing
mplmon2.k φKD
mplmon2.x φXB
Assertion mplmon2 φX·˙yDify=K1˙0˙=yDify=KX0˙

Proof

Step Hyp Ref Expression
1 mplmon2.p P=ImPolyR
2 mplmon2.v ·˙=P
3 mplmon2.d D=f0I|f-1Fin
4 mplmon2.o 1˙=1R
5 mplmon2.z 0˙=0R
6 mplmon2.b B=BaseR
7 mplmon2.i φIW
8 mplmon2.r φRRing
9 mplmon2.k φKD
10 mplmon2.x φXB
11 eqid BaseP=BaseP
12 eqid R=R
13 1 11 5 4 3 7 8 9 mplmon φyDify=K1˙0˙BaseP
14 1 2 6 11 12 3 10 13 mplvsca φX·˙yDify=K1˙0˙=D×XRfyDify=K1˙0˙
15 ovex 0IV
16 3 15 rabex2 DV
17 16 a1i φDV
18 10 adantr φyDXB
19 4 fvexi 1˙V
20 5 fvexi 0˙V
21 19 20 ifex ify=K1˙0˙V
22 21 a1i φyDify=K1˙0˙V
23 fconstmpt D×X=yDX
24 23 a1i φD×X=yDX
25 eqidd φyDify=K1˙0˙=yDify=K1˙0˙
26 17 18 22 24 25 offval2 φD×XRfyDify=K1˙0˙=yDXRify=K1˙0˙
27 oveq2 1˙=ify=K1˙0˙XR1˙=XRify=K1˙0˙
28 27 eqeq1d 1˙=ify=K1˙0˙XR1˙=ify=KX0˙XRify=K1˙0˙=ify=KX0˙
29 oveq2 0˙=ify=K1˙0˙XR0˙=XRify=K1˙0˙
30 29 eqeq1d 0˙=ify=K1˙0˙XR0˙=ify=KX0˙XRify=K1˙0˙=ify=KX0˙
31 6 12 4 ringridm RRingXBXR1˙=X
32 8 10 31 syl2anc φXR1˙=X
33 iftrue y=Kify=KX0˙=X
34 33 eqcomd y=KX=ify=KX0˙
35 32 34 sylan9eq φy=KXR1˙=ify=KX0˙
36 6 12 5 ringrz RRingXBXR0˙=0˙
37 8 10 36 syl2anc φXR0˙=0˙
38 iffalse ¬y=Kify=KX0˙=0˙
39 38 eqcomd ¬y=K0˙=ify=KX0˙
40 37 39 sylan9eq φ¬y=KXR0˙=ify=KX0˙
41 28 30 35 40 ifbothda φXRify=K1˙0˙=ify=KX0˙
42 41 mpteq2dv φyDXRify=K1˙0˙=yDify=KX0˙
43 14 26 42 3eqtrd φX·˙yDify=K1˙0˙=yDify=KX0˙