Metamath Proof Explorer


Theorem deg1n0ima

Description: Degree image of a set of polynomials which does not include zero. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses deg1z.d D=deg1R
deg1z.p P=Poly1R
deg1z.z 0˙=0P
deg1nn0cl.b B=BaseP
Assertion deg1n0ima RRingDB0˙0

Proof

Step Hyp Ref Expression
1 deg1z.d D=deg1R
2 deg1z.p P=Poly1R
3 deg1z.z 0˙=0P
4 deg1nn0cl.b B=BaseP
5 simpl RRingxB0˙RRing
6 eldifi xB0˙xB
7 6 adantl RRingxB0˙xB
8 eldifsni xB0˙x0˙
9 8 adantl RRingxB0˙x0˙
10 1 2 3 4 deg1nn0cl RRingxBx0˙Dx0
11 5 7 9 10 syl3anc RRingxB0˙Dx0
12 11 ralrimiva RRingxB0˙Dx0
13 1 2 4 deg1xrf D:B*
14 ffun D:B*FunD
15 13 14 ax-mp FunD
16 difss B0˙B
17 13 fdmi domD=B
18 16 17 sseqtrri B0˙domD
19 funimass4 FunDB0˙domDDB0˙0xB0˙Dx0
20 15 18 19 mp2an DB0˙0xB0˙Dx0
21 12 20 sylibr RRingDB0˙0