Metamath Proof Explorer


Theorem coe1tmfv1

Description: Nonzero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses coe1tm.z 0˙=0R
coe1tm.k K=BaseR
coe1tm.p P=Poly1R
coe1tm.x X=var1R
coe1tm.m ·˙=P
coe1tm.n N=mulGrpP
coe1tm.e ×˙=N
Assertion coe1tmfv1 RRingCKD0coe1C·˙D×˙XD=C

Proof

Step Hyp Ref Expression
1 coe1tm.z 0˙=0R
2 coe1tm.k K=BaseR
3 coe1tm.p P=Poly1R
4 coe1tm.x X=var1R
5 coe1tm.m ·˙=P
6 coe1tm.n N=mulGrpP
7 coe1tm.e ×˙=N
8 1 2 3 4 5 6 7 coe1tm RRingCKD0coe1C·˙D×˙X=x0ifx=DC0˙
9 8 fveq1d RRingCKD0coe1C·˙D×˙XD=x0ifx=DC0˙D
10 eqid x0ifx=DC0˙=x0ifx=DC0˙
11 iftrue x=Difx=DC0˙=C
12 simp3 RRingCKD0D0
13 simp2 RRingCKD0CK
14 10 11 12 13 fvmptd3 RRingCKD0x0ifx=DC0˙D=C
15 9 14 eqtrd RRingCKD0coe1C·˙D×˙XD=C