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	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
	deg1nn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1ldgdomn.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
	deg1ldgdomn.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
Assertion	deg1ldgdomn	⊢ ( ( 𝑅 ∈ Domn ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
4		deg1nn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		deg1ldgdomn.e	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
6		deg1ldgdomn.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
7		simp1	⊢ ( ( 𝑅 ∈ Domn ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → 𝑅 ∈ Domn )
8		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9	6 4 2 8	coe1f	⊢ ( 𝐹 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
10	9	3ad2ant2	⊢ ( ( 𝑅 ∈ Domn ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
11		domnring	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
12	1 2 3 4	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
13	11 12	syl3an1	⊢ ( ( 𝑅 ∈ Domn ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
14	10 13	ffvelrnd	⊢ ( ( 𝑅 ∈ Domn ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝑅 ) )
15		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
16	1 2 3 4 15 6	deg1ldg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) )
17	11 16	syl3an1	⊢ ( ( 𝑅 ∈ Domn ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) )
18	8 5 15	domnrrg	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝐸 )
19	7 14 17 18	syl3anc	⊢ ( ( 𝑅 ∈ Domn ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝐸 )