Metamath Proof Explorer

Theorem ply1domn

Description: Corollary of deg1mul2 : the univariate polynomials over a domain are a domain. This is true for multivariate but with a much more complicated proof. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypothesis ply1domn.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
Assertion ply1domn ( 𝑅 ∈ Domn → 𝑃 ∈ Domn )

Proof

Step Hyp Ref Expression
1 ply1domn.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
3 1 ply1nz ⊢ ( 𝑅 ∈ NzRing → 𝑃 ∈ NzRing )
4 2 3 syl ⊢ ( 𝑅 ∈ Domn → 𝑃 ∈ NzRing )
5 neanior ⊢ ( ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ↔ ¬ ( 𝑥 = ( 0g ‘ 𝑃 ) ∨ 𝑦 = ( 0g ‘ 𝑃 ) ) )
6 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
7 eqid ⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
8 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
9 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
10 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
11 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
12 11 ad2antrr ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → 𝑅 ∈ Ring )
13 simplrl ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
14 simprl ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → 𝑥 ≠ ( 0g ‘ 𝑃 ) )
15 simpll ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → 𝑅 ∈ Domn )
16 eqid ⊢ ( coe1 ‘ 𝑥 ) = ( coe1 ‘ 𝑥 )
17 6 1 10 8 7 16 deg1ldgdomn ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑃 ) ) → ( ( coe1 ‘ 𝑥 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ ( RLReg ‘ 𝑅 ) )
18 15 13 14 17 syl3anc ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → ( ( coe1 ‘ 𝑥 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝑥 ) ) ∈ ( RLReg ‘ 𝑅 ) )
19 simplrr ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑃 ) )
20 simprr ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → 𝑦 ≠ ( 0g ‘ 𝑃 ) )
21 6 1 7 8 9 10 12 13 14 18 19 20 deg1mul2 ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑥 ) + ( ( deg1 ‘ 𝑅 ) ‘ 𝑦 ) ) )
22 6 1 10 8 deg1nn0cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑃 ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑥 ) ∈ ℕ0 )
23 12 13 14 22 syl3anc ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑥 ) ∈ ℕ0 )
24 6 1 10 8 deg1nn0cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑦 ) ∈ ℕ0 )
25 12 19 20 24 syl3anc ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑦 ) ∈ ℕ0 )
26 23 25 nn0addcld ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑥 ) + ( ( deg1 ‘ 𝑅 ) ‘ 𝑦 ) ) ∈ ℕ0 )
27 21 26 eqeltrd ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) ∈ ℕ0 )
28 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
29 11 28 syl ⊢ ( 𝑅 ∈ Domn → 𝑃 ∈ Ring )
30 29 ad2antrr ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → 𝑃 ∈ Ring )
31 8 9 ringcl ⊢ ( ( 𝑃 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ ( Base ‘ 𝑃 ) )
32 30 13 19 31 syl3anc ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ ( Base ‘ 𝑃 ) )
33 6 1 10 8 deg1nn0clb ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ≠ ( 0g ‘ 𝑃 ) ↔ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) ∈ ℕ0 ) )
34 12 32 33 syl2anc ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ≠ ( 0g ‘ 𝑃 ) ↔ ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) ∈ ℕ0 ) )
35 27 34 mpbird ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) ∧ ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ≠ ( 0g ‘ 𝑃 ) )
36 35 ex ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝑥 ≠ ( 0g ‘ 𝑃 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ≠ ( 0g ‘ 𝑃 ) ) )
37 5 36 syl5bir ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( ¬ ( 𝑥 = ( 0g ‘ 𝑃 ) ∨ 𝑦 = ( 0g ‘ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ≠ ( 0g ‘ 𝑃 ) ) )
38 37 necon4bd ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 0g ‘ 𝑃 ) → ( 𝑥 = ( 0g ‘ 𝑃 ) ∨ 𝑦 = ( 0g ‘ 𝑃 ) ) ) )
39 38 ralrimivva ⊢ ( 𝑅 ∈ Domn → ∀ 𝑥 ∈ ( Base ‘ 𝑃 ) ∀ 𝑦 ∈ ( Base ‘ 𝑃 ) ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 0g ‘ 𝑃 ) → ( 𝑥 = ( 0g ‘ 𝑃 ) ∨ 𝑦 = ( 0g ‘ 𝑃 ) ) ) )
40 8 9 10 isdomn ⊢ ( 𝑃 ∈ Domn ↔ ( 𝑃 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑃 ) ∀ 𝑦 ∈ ( Base ‘ 𝑃 ) ( ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 0g ‘ 𝑃 ) → ( 𝑥 = ( 0g ‘ 𝑃 ) ∨ 𝑦 = ( 0g ‘ 𝑃 ) ) ) ) )
41 4 39 40 sylanbrc ⊢ ( 𝑅 ∈ Domn → 𝑃 ∈ Domn )