Theorem 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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	fta1b.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	fta1b.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	fta1b.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	fta1b.w	⊢ 𝑊 = ( 0g ‘ 𝑅 )
	fta1b.z	⊢ 0 = ( 0g ‘ 𝑃 )
Assertion	fta1b	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fta1b.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		fta1b.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		fta1b.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
4		fta1b.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
5		fta1b.w	⊢ 𝑊 = ( 0g ‘ 𝑅 )
6		fta1b.z	⊢ 0 = ( 0g ‘ 𝑃 )
7		isidom	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
8	7	simplbi	⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ CRing )
9	7	simprbi	⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ Domn )
10		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
11	9 10	syl	⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ NzRing )
12		simpl	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑅 ∈ IDomn )
13		eldifsn	⊢ ( 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑓 ∈ 𝐵 ∧ 𝑓 ≠ 0 ) )
14	13	simplbi	⊢ ( 𝑓 ∈ ( 𝐵 ∖ { 0 } ) → 𝑓 ∈ 𝐵 )
15	14	adantl	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑓 ∈ 𝐵 )
16	13	simprbi	⊢ ( 𝑓 ∈ ( 𝐵 ∖ { 0 } ) → 𝑓 ≠ 0 )
17	16	adantl	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑓 ≠ 0 )
18	1 2 3 4 5 6 12 15 17	fta1g	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) )
19	18	ralrimiva	⊢ ( 𝑅 ∈ IDomn → ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) )
20	8 11 19	3jca	⊢ ( 𝑅 ∈ IDomn → ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) )
21		simp1	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) → 𝑅 ∈ CRing )
22		simp2	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) → 𝑅 ∈ NzRing )
23		df-ne	⊢ ( 𝑥 ≠ 𝑊 ↔ ¬ 𝑥 = 𝑊 )
24		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
25		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
26		eqid	⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
27		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
28		simpll1	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 ∧ 𝑥 ≠ 𝑊 ) ) → 𝑅 ∈ CRing )
29		simplrl	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 ∧ 𝑥 ≠ 𝑊 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
30		simplrr	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 ∧ 𝑥 ≠ 𝑊 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
31		simprl	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 ∧ 𝑥 ≠ 𝑊 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 )
32		simprr	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 ∧ 𝑥 ≠ 𝑊 ) ) → 𝑥 ≠ 𝑊 )
33		simpll3	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 ∧ 𝑥 ≠ 𝑊 ) ) → ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) )
34		fveq2	⊢ ( 𝑓 = ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) → ( 𝑂 ‘ 𝑓 ) = ( 𝑂 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) )
35	34	cnveqd	⊢ ( 𝑓 = ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) → ◡ ( 𝑂 ‘ 𝑓 ) = ◡ ( 𝑂 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) )
36	35	imaeq1d	⊢ ( 𝑓 = ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) → ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) = ( ◡ ( 𝑂 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) “ { 𝑊 } ) )
37	36	fveq2d	⊢ ( 𝑓 = ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) → ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) = ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) “ { 𝑊 } ) ) )
38		fveq2	⊢ ( 𝑓 = ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) → ( 𝐷 ‘ 𝑓 ) = ( 𝐷 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) )
39	37 38	breq12d	⊢ ( 𝑓 = ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) → ( ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ↔ ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ) )
40	39	rspccv	⊢ ( ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ∈ ( 𝐵 ∖ { 0 } ) → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ) )
41	33 40	syl	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 ∧ 𝑥 ≠ 𝑊 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ∈ ( 𝐵 ∖ { 0 } ) → ( ♯ ‘ ( ◡ ( 𝑂 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ) )
42	1 2 3 4 5 6 24 25 26 27 28 29 30 31 32 41	fta1blem	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 ∧ 𝑥 ≠ 𝑊 ) ) → 𝑦 = 𝑊 )
43	42	expr	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 ) → ( 𝑥 ≠ 𝑊 → 𝑦 = 𝑊 ) )
44	23 43	biimtrrid	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 ) → ( ¬ 𝑥 = 𝑊 → 𝑦 = 𝑊 ) )
45	44	orrd	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 ) → ( 𝑥 = 𝑊 ∨ 𝑦 = 𝑊 ) )
46	45	ex	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 → ( 𝑥 = 𝑊 ∨ 𝑦 = 𝑊 ) ) )
47	46	ralrimivva	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 → ( 𝑥 = 𝑊 ∨ 𝑦 = 𝑊 ) ) )
48	24 25 5	isdomn	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑊 → ( 𝑥 = 𝑊 ∨ 𝑦 = 𝑊 ) ) ) )
49	22 47 48	sylanbrc	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) → 𝑅 ∈ Domn )
50	21 49 7	sylanbrc	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) → 𝑅 ∈ IDomn )
51	20 50	impbii	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ NzRing ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ { 0 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) )