Theorem deg1ldgdomn

Description: A nonzero univariate polynomial over a domain always has a nonzero-divisor leading coefficient. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	deg1z.d	|- D = ( deg1 ` R )
	deg1z.p	|- P = ( Poly1 ` R )
	deg1z.z	|- .0. = ( 0g ` P )
	deg1nn0cl.b	|- B = ( Base ` P )
	deg1ldgdomn.e	|- E = ( RLReg ` R )
	deg1ldgdomn.a	|- A = ( coe1 ` F )
Assertion	deg1ldgdomn	|- ( ( R e. Domn /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) e. E )

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	|- D = ( deg1 ` R )
2		deg1z.p	|- P = ( Poly1 ` R )
3		deg1z.z	|- .0. = ( 0g ` P )
4		deg1nn0cl.b	|- B = ( Base ` P )
5		deg1ldgdomn.e	|- E = ( RLReg ` R )
6		deg1ldgdomn.a	|- A = ( coe1 ` F )
7		simp1	|- ( ( R e. Domn /\ F e. B /\ F =/= .0. ) -> R e. Domn )
8		eqid	|- ( Base ` R ) = ( Base ` R )
9	6 4 2 8	coe1f	|- ( F e. B -> A : NN0 --> ( Base ` R ) )
10	9	3ad2ant2	|- ( ( R e. Domn /\ F e. B /\ F =/= .0. ) -> A : NN0 --> ( Base ` R ) )
11		domnring	|- ( R e. Domn -> R e. Ring )
12	1 2 3 4	deg1nn0cl	|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )
13	11 12	syl3an1	|- ( ( R e. Domn /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )
14	10 13	ffvelrnd	|- ( ( R e. Domn /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) e. ( Base ` R ) )
15		eqid	|- ( 0g ` R ) = ( 0g ` R )
16	1 2 3 4 15 6	deg1ldg	|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) =/= ( 0g ` R ) )
17	11 16	syl3an1	|- ( ( R e. Domn /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) =/= ( 0g ` R ) )
18	8 5 15	domnrrg	|- ( ( R e. Domn /\ ( A ` ( D ` F ) ) e. ( Base ` R ) /\ ( A ` ( D ` F ) ) =/= ( 0g ` R ) ) -> ( A ` ( D ` F ) ) e. E )
19	7 14 17 18	syl3anc	|- ( ( R e. Domn /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) e. E )