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 
|- P = ( Poly1 ` R )
fta1b.b 
|- B = ( Base ` P )
fta1b.d 
|- D = ( deg1 ` R )
fta1b.o 
|- O = ( eval1 ` R )
fta1b.w 
|- W = ( 0g ` R )
fta1b.z 
|- .0. = ( 0g ` P )
Assertion fta1b 
|- ( R e. IDomn <-> ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) )

Proof

Step Hyp Ref Expression
1 fta1b.p 
 |-  P = ( Poly1 ` R )
2 fta1b.b 
 |-  B = ( Base ` P )
3 fta1b.d 
 |-  D = ( deg1 ` R )
4 fta1b.o 
 |-  O = ( eval1 ` R )
5 fta1b.w 
 |-  W = ( 0g ` R )
6 fta1b.z 
 |-  .0. = ( 0g ` P )
7 isidom 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
8 7 simplbi 
 |-  ( R e. IDomn -> R e. CRing )
9 7 simprbi 
 |-  ( R e. IDomn -> R e. Domn )
10 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
11 9 10 syl 
 |-  ( R e. IDomn -> R e. NzRing )
12 simpl 
 |-  ( ( R e. IDomn /\ f e. ( B \ { .0. } ) ) -> R e. IDomn )
13 eldifsn 
 |-  ( f e. ( B \ { .0. } ) <-> ( f e. B /\ f =/= .0. ) )
14 13 simplbi 
 |-  ( f e. ( B \ { .0. } ) -> f e. B )
15 14 adantl 
 |-  ( ( R e. IDomn /\ f e. ( B \ { .0. } ) ) -> f e. B )
16 13 simprbi 
 |-  ( f e. ( B \ { .0. } ) -> f =/= .0. )
17 16 adantl 
 |-  ( ( R e. IDomn /\ f e. ( B \ { .0. } ) ) -> f =/= .0. )
18 1 2 3 4 5 6 12 15 17 fta1g 
 |-  ( ( R e. IDomn /\ f e. ( B \ { .0. } ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) )
19 18 ralrimiva 
 |-  ( R e. IDomn -> A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) )
20 8 11 19 3jca 
 |-  ( R e. IDomn -> ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) )
21 simp1 
 |-  ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) -> R e. CRing )
22 simp2 
 |-  ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) -> R e. NzRing )
23 df-ne 
 |-  ( x =/= W <-> -. x = W )
24 eqid 
 |-  ( Base ` R ) = ( Base ` R )
25 eqid 
 |-  ( .r ` R ) = ( .r ` R )
26 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
27 eqid 
 |-  ( .s ` P ) = ( .s ` P )
28 simpll1 
 |-  ( ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) /\ ( ( x ( .r ` R ) y ) = W /\ x =/= W ) ) -> R e. CRing )
29 simplrl 
 |-  ( ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) /\ ( ( x ( .r ` R ) y ) = W /\ x =/= W ) ) -> x e. ( Base ` R ) )
30 simplrr 
 |-  ( ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) /\ ( ( x ( .r ` R ) y ) = W /\ x =/= W ) ) -> y e. ( Base ` R ) )
31 simprl 
 |-  ( ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) /\ ( ( x ( .r ` R ) y ) = W /\ x =/= W ) ) -> ( x ( .r ` R ) y ) = W )
32 simprr 
 |-  ( ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) /\ ( ( x ( .r ` R ) y ) = W /\ x =/= W ) ) -> x =/= W )
33 simpll3 
 |-  ( ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) /\ ( ( x ( .r ` R ) y ) = W /\ x =/= W ) ) -> A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) )
34 fveq2 
 |-  ( f = ( x ( .s ` P ) ( var1 ` R ) ) -> ( O ` f ) = ( O ` ( x ( .s ` P ) ( var1 ` R ) ) ) )
35 34 cnveqd 
 |-  ( f = ( x ( .s ` P ) ( var1 ` R ) ) -> `' ( O ` f ) = `' ( O ` ( x ( .s ` P ) ( var1 ` R ) ) ) )
36 35 imaeq1d 
 |-  ( f = ( x ( .s ` P ) ( var1 ` R ) ) -> ( `' ( O ` f ) " { W } ) = ( `' ( O ` ( x ( .s ` P ) ( var1 ` R ) ) ) " { W } ) )
37 36 fveq2d 
 |-  ( f = ( x ( .s ` P ) ( var1 ` R ) ) -> ( # ` ( `' ( O ` f ) " { W } ) ) = ( # ` ( `' ( O ` ( x ( .s ` P ) ( var1 ` R ) ) ) " { W } ) ) )
38 fveq2 
 |-  ( f = ( x ( .s ` P ) ( var1 ` R ) ) -> ( D ` f ) = ( D ` ( x ( .s ` P ) ( var1 ` R ) ) ) )
39 37 38 breq12d 
 |-  ( f = ( x ( .s ` P ) ( var1 ` R ) ) -> ( ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) <-> ( # ` ( `' ( O ` ( x ( .s ` P ) ( var1 ` R ) ) ) " { W } ) ) <_ ( D ` ( x ( .s ` P ) ( var1 ` R ) ) ) ) )
40 39 rspccv 
 |-  ( A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) -> ( ( x ( .s ` P ) ( var1 ` R ) ) e. ( B \ { .0. } ) -> ( # ` ( `' ( O ` ( x ( .s ` P ) ( var1 ` R ) ) ) " { W } ) ) <_ ( D ` ( x ( .s ` P ) ( var1 ` R ) ) ) ) )
41 33 40 syl 
 |-  ( ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) /\ ( ( x ( .r ` R ) y ) = W /\ x =/= W ) ) -> ( ( x ( .s ` P ) ( var1 ` R ) ) e. ( B \ { .0. } ) -> ( # ` ( `' ( O ` ( x ( .s ` P ) ( var1 ` R ) ) ) " { W } ) ) <_ ( D ` ( x ( .s ` P ) ( var1 ` R ) ) ) ) )
42 1 2 3 4 5 6 24 25 26 27 28 29 30 31 32 41 fta1blem 
 |-  ( ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) /\ ( ( x ( .r ` R ) y ) = W /\ x =/= W ) ) -> y = W )
43 42 expr 
 |-  ( ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) /\ ( x ( .r ` R ) y ) = W ) -> ( x =/= W -> y = W ) )
44 23 43 syl5bir 
 |-  ( ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) /\ ( x ( .r ` R ) y ) = W ) -> ( -. x = W -> y = W ) )
45 44 orrd 
 |-  ( ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) /\ ( x ( .r ` R ) y ) = W ) -> ( x = W \/ y = W ) )
46 45 ex 
 |-  ( ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( x ( .r ` R ) y ) = W -> ( x = W \/ y = W ) ) )
47 46 ralrimivva 
 |-  ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = W -> ( x = W \/ y = W ) ) )
48 24 25 5 isdomn 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = W -> ( x = W \/ y = W ) ) ) )
49 22 47 48 sylanbrc 
 |-  ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) -> R e. Domn )
50 21 49 7 sylanbrc 
 |-  ( ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) -> R e. IDomn )
51 20 50 impbii 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. NzRing /\ A. f e. ( B \ { .0. } ) ( # ` ( `' ( O ` f ) " { W } ) ) <_ ( D ` f ) ) )