fta1b

Description: The assumption that R be a domain in fta1g is necessary. Here we show that the statement is strong enough to prove that R is a domain. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	fta1b.p	$⊢ P = {Poly}_{1} (R)$
	fta1b.b	$⊢ B = {Base}_{P}$
	fta1b.d	$⊢ D = \deg_{1} (R)$
	fta1b.o	$⊢ O = {eval}_{1} (R)$
	fta1b.w	$⊢ W = 0_{R}$
	fta1b.z	$⊢ \underset{˙}{0} = 0_{P}$
Assertion	fta1b	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f))$

Proof

Step	Hyp	Ref	Expression
1		fta1b.p	$⊢ P = {Poly}_{1} (R)$
2		fta1b.b	$⊢ B = {Base}_{P}$
3		fta1b.d	$⊢ D = \deg_{1} (R)$
4		fta1b.o	$⊢ O = {eval}_{1} (R)$
5		fta1b.w	$⊢ W = 0_{R}$
6		fta1b.z	$⊢ \underset{˙}{0} = 0_{P}$
7		isidom	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in Domn)$
8	7	simplbi	$⊢ R \in IDomn \to R \in CRing$
9	7	simprbi	$⊢ R \in IDomn \to R \in Domn$
10		domnnzr	$⊢ R \in Domn \to R \in NzRing$
11	9 10	syl	$⊢ R \in IDomn \to R \in NzRing$
12		simpl	$⊢ (R \in IDomn \land f \in (B ∖ \{\underset{˙}{0}\})) \to R \in IDomn$
13		eldifsn	$⊢ f \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (f \in B \land f \neq \underset{˙}{0})$
14	13	simplbi	$⊢ f \in (B ∖ \{\underset{˙}{0}\}) \to f \in B$
15	14	adantl	$⊢ (R \in IDomn \land f \in (B ∖ \{\underset{˙}{0}\})) \to f \in B$
16	13	simprbi	$⊢ f \in (B ∖ \{\underset{˙}{0}\}) \to f \neq \underset{˙}{0}$
17	16	adantl	$⊢ (R \in IDomn \land f \in (B ∖ \{\underset{˙}{0}\})) \to f \neq \underset{˙}{0}$
18	1 2 3 4 5 6 12 15 17	fta1g	$⊢ (R \in IDomn \land f \in (B ∖ \{\underset{˙}{0}\})) \to \|{O (f)}^{-1} [\{W\}]\| \leq D (f)$
19	18	ralrimiva	$⊢ R \in IDomn \to \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)$
20	8 11 19	3jca	$⊢ R \in IDomn \to (R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f))$
21		simp1	$⊢ (R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \to R \in CRing$
22		simp2	$⊢ (R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \to R \in NzRing$
23		df-ne	$⊢ x \neq W \leftrightarrow \neg x = W$
24		eqid	$⊢ {Base}_{R} = {Base}_{R}$
25		eqid	$⊢ \cdot_{R} = \cdot_{R}$
26		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
27		eqid	$⊢ \cdot_{P} = \cdot_{P}$
28		simpll1	$⊢ (((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \land (x \cdot_{R} y = W \land x \neq W)) \to R \in CRing$
29		simplrl	$⊢ (((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \land (x \cdot_{R} y = W \land x \neq W)) \to x \in {Base}_{R}$
30		simplrr	$⊢ (((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \land (x \cdot_{R} y = W \land x \neq W)) \to y \in {Base}_{R}$
31		simprl	$⊢ (((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \land (x \cdot_{R} y = W \land x \neq W)) \to x \cdot_{R} y = W$
32		simprr	$⊢ (((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \land (x \cdot_{R} y = W \land x \neq W)) \to x \neq W$
33		simpll3	$⊢ (((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \land (x \cdot_{R} y = W \land x \neq W)) \to \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)$
34		fveq2	$⊢ f = x \cdot_{P} {var}_{1} (R) \to O (f) = O (x \cdot_{P} {var}_{1} (R))$
35	34	cnveqd	$⊢ f = x \cdot_{P} {var}_{1} (R) \to {O (f)}^{-1} = {O (x \cdot_{P} {var}_{1} (R))}^{-1}$
36	35	imaeq1d	$⊢ f = x \cdot_{P} {var}_{1} (R) \to {O (f)}^{-1} [\{W\}] = {O (x \cdot_{P} {var}_{1} (R))}^{-1} [\{W\}]$
37	36	fveq2d	$⊢ f = x \cdot_{P} {var}_{1} (R) \to \|{O (f)}^{-1} [\{W\}]\| = \|{O (x \cdot_{P} {var}_{1} (R))}^{-1} [\{W\}]\|$
38		fveq2	$⊢ f = x \cdot_{P} {var}_{1} (R) \to D (f) = D (x \cdot_{P} {var}_{1} (R))$
39	37 38	breq12d	$⊢ f = x \cdot_{P} {var}_{1} (R) \to (\|{O (f)}^{-1} [\{W\}]\| \leq D (f) \leftrightarrow \|{O (x \cdot_{P} {var}_{1} (R))}^{-1} [\{W\}]\| \leq D (x \cdot_{P} {var}_{1} (R)))$
40	39	rspccv	$⊢ \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f) \to (x \cdot_{P} {var}_{1} (R) \in (B ∖ \{\underset{˙}{0}\}) \to \|{O (x \cdot_{P} {var}_{1} (R))}^{-1} [\{W\}]\| \leq D (x \cdot_{P} {var}_{1} (R)))$
41	33 40	syl	$⊢ (((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \land (x \cdot_{R} y = W \land x \neq W)) \to (x \cdot_{P} {var}_{1} (R) \in (B ∖ \{\underset{˙}{0}\}) \to \|{O (x \cdot_{P} {var}_{1} (R))}^{-1} [\{W\}]\| \leq D (x \cdot_{P} {var}_{1} (R)))$
42	1 2 3 4 5 6 24 25 26 27 28 29 30 31 32 41	fta1blem	$⊢ (((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \land (x \cdot_{R} y = W \land x \neq W)) \to y = W$
43	42	expr	$⊢ (((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \land x \cdot_{R} y = W) \to (x \neq W \to y = W)$
44	23 43	biimtrrid	$⊢ (((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \land x \cdot_{R} y = W) \to (\neg x = W \to y = W)$
45	44	orrd	$⊢ (((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \land x \cdot_{R} y = W) \to (x = W \lor y = W)$
46	45	ex	$⊢ ((R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to (x \cdot_{R} y = W \to (x = W \lor y = W))$
47	46	ralrimivva	$⊢ (R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \to \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y = W \to (x = W \lor y = W))$
48	24 25 5	isdomn	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (x \cdot_{R} y = W \to (x = W \lor y = W)))$
49	22 47 48	sylanbrc	$⊢ (R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \to R \in Domn$
50	21 49 7	sylanbrc	$⊢ (R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f)) \to R \in IDomn$
51	20 50	impbii	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in NzRing \land \forall f \in (B ∖ \{\underset{˙}{0}\}) \|{O (f)}^{-1} [\{W\}]\| \leq D (f))$

Metamath Proof Explorer

Theorem fta1b

Proof