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	$⊢ P = {Poly}_{1} (R)$
	Assertion	ply1domn	$⊢ R \in Domn \to P \in Domn$

Proof

Step	Hyp	Ref	Expression
1		ply1domn.p	$⊢ P = {Poly}_{1} (R)$
2		domnnzr	$⊢ R \in Domn \to R \in NzRing$
3	1	ply1nz	$⊢ R \in NzRing \to P \in NzRing$
4	2 3	syl	$⊢ R \in Domn \to P \in NzRing$
5		neanior	$⊢ (x \neq 0_{P} \land y \neq 0_{P}) \leftrightarrow \neg (x = 0_{P} \lor y = 0_{P})$
6		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
7		eqid	$⊢ RLReg (R) = RLReg (R)$
8		eqid	$⊢ {Base}_{P} = {Base}_{P}$
9		eqid	$⊢ \cdot_{P} = \cdot_{P}$
10		eqid	$⊢ 0_{P} = 0_{P}$
11		domnring	$⊢ R \in Domn \to R \in Ring$
12	11	ad2antrr	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to R \in Ring$
13		simplrl	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to x \in {Base}_{P}$
14		simprl	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to x \neq 0_{P}$
15		simpll	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to R \in Domn$
16		eqid	$⊢ {coe}_{1} (x) = {coe}_{1} (x)$
17	6 1 10 8 7 16	deg1ldgdomn	$⊢ (R \in Domn \land x \in {Base}_{P} \land x \neq 0_{P}) \to {coe}_{1} (x) (\deg_{1} (R) (x)) \in RLReg (R)$
18	15 13 14 17	syl3anc	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to {coe}_{1} (x) (\deg_{1} (R) (x)) \in RLReg (R)$
19		simplrr	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to y \in {Base}_{P}$
20		simprr	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to y \neq 0_{P}$
21	6 1 7 8 9 10 12 13 14 18 19 20	deg1mul2	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to \deg_{1} (R) (x \cdot_{P} y) = \deg_{1} (R) (x) + \deg_{1} (R) (y)$
22	6 1 10 8	deg1nn0cl	$⊢ (R \in Ring \land x \in {Base}_{P} \land x \neq 0_{P}) \to \deg_{1} (R) (x) \in ℕ_{0}$
23	12 13 14 22	syl3anc	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to \deg_{1} (R) (x) \in ℕ_{0}$
24	6 1 10 8	deg1nn0cl	$⊢ (R \in Ring \land y \in {Base}_{P} \land y \neq 0_{P}) \to \deg_{1} (R) (y) \in ℕ_{0}$
25	12 19 20 24	syl3anc	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to \deg_{1} (R) (y) \in ℕ_{0}$
26	23 25	nn0addcld	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to \deg_{1} (R) (x) + \deg_{1} (R) (y) \in ℕ_{0}$
27	21 26	eqeltrd	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to \deg_{1} (R) (x \cdot_{P} y) \in ℕ_{0}$
28	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
29	11 28	syl	$⊢ R \in Domn \to P \in Ring$
30	29	ad2antrr	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to P \in Ring$
31	8 9	ringcl	$⊢ (P \in Ring \land x \in {Base}_{P} \land y \in {Base}_{P}) \to x \cdot_{P} y \in {Base}_{P}$
32	30 13 19 31	syl3anc	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to x \cdot_{P} y \in {Base}_{P}$
33	6 1 10 8	deg1nn0clb	$⊢ (R \in Ring \land x \cdot_{P} y \in {Base}_{P}) \to (x \cdot_{P} y \neq 0_{P} \leftrightarrow \deg_{1} (R) (x \cdot_{P} y) \in ℕ_{0})$
34	12 32 33	syl2anc	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to (x \cdot_{P} y \neq 0_{P} \leftrightarrow \deg_{1} (R) (x \cdot_{P} y) \in ℕ_{0})$
35	27 34	mpbird	$⊢ ((R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \land (x \neq 0_{P} \land y \neq 0_{P})) \to x \cdot_{P} y \neq 0_{P}$
36	35	ex	$⊢ (R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to ((x \neq 0_{P} \land y \neq 0_{P}) \to x \cdot_{P} y \neq 0_{P})$
37	5 36	biimtrrid	$⊢ (R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to (\neg (x = 0_{P} \lor y = 0_{P}) \to x \cdot_{P} y \neq 0_{P})$
38	37	necon4bd	$⊢ (R \in Domn \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to (x \cdot_{P} y = 0_{P} \to (x = 0_{P} \lor y = 0_{P}))$
39	38	ralrimivva	$⊢ R \in Domn \to \forall x \in {Base}_{P} \forall y \in {Base}_{P} (x \cdot_{P} y = 0_{P} \to (x = 0_{P} \lor y = 0_{P}))$
40	8 9 10	isdomn	$⊢ P \in Domn \leftrightarrow (P \in NzRing \land \forall x \in {Base}_{P} \forall y \in {Base}_{P} (x \cdot_{P} y = 0_{P} \to (x = 0_{P} \lor y = 0_{P})))$
41	4 39 40	sylanbrc	$⊢ R \in Domn \to P \in Domn$

Metamath Proof Explorer

Theorem ply1domn

Proof