This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmd ⊢ ( ( 𝑅 ∈ 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 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝐸 )