Metamath Proof Explorer

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 syl5bir ⊢ ( ( ( ( 𝑅 ∈ 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 } ) ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝑓 ) ) )