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 = 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 0 ˙ = 0 P
Assertion fta1b R IDomn R CRing R NzRing f B 0 ˙ O f -1 W 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 0 ˙ = 0 P
7 isidom R IDomn R CRing R Domn
8 7 simplbi R IDomn R CRing
9 7 simprbi R IDomn R Domn
10 domnnzr R Domn R NzRing
11 9 10 syl R IDomn R NzRing
12 simpl R IDomn f B 0 ˙ R IDomn
13 eldifsn f B 0 ˙ f B f 0 ˙
14 13 simplbi f B 0 ˙ f B
15 14 adantl R IDomn f B 0 ˙ f B
16 13 simprbi f B 0 ˙ f 0 ˙
17 16 adantl R IDomn f B 0 ˙ f 0 ˙
18 1 2 3 4 5 6 12 15 17 fta1g R IDomn f B 0 ˙ O f -1 W D f
19 18 ralrimiva R IDomn f B 0 ˙ O f -1 W D f
20 8 11 19 3jca R IDomn R CRing R NzRing f B 0 ˙ O f -1 W D f
21 simp1 R CRing R NzRing f B 0 ˙ O f -1 W D f R CRing
22 simp2 R CRing R NzRing f B 0 ˙ O f -1 W D f R NzRing
23 df-ne x W ¬ x = W
24 eqid Base R = Base R
25 eqid R = R
26 eqid var 1 R = var 1 R
27 eqid P = P
28 simpll1 R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x W R CRing
29 simplrl R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x W x Base R
30 simplrr R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x W y Base R
31 simprl R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x W x R y = W
32 simprr R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x W x W
33 simpll3 R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x W f B 0 ˙ O f -1 W D f
34 fveq2 f = x P var 1 R O f = O x P var 1 R
35 34 cnveqd f = x P var 1 R O f -1 = O x P var 1 R -1
36 35 imaeq1d f = x P var 1 R O f -1 W = O x P var 1 R -1 W
37 36 fveq2d f = x P var 1 R O f -1 W = O x P var 1 R -1 W
38 fveq2 f = x P var 1 R D f = D x P var 1 R
39 37 38 breq12d f = x P var 1 R O f -1 W D f O x P var 1 R -1 W D x P var 1 R
40 39 rspccv f B 0 ˙ O f -1 W D f x P var 1 R B 0 ˙ O x P var 1 R -1 W D x P var 1 R
41 33 40 syl R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x W x P var 1 R B 0 ˙ O x P var 1 R -1 W D x P var 1 R
42 1 2 3 4 5 6 24 25 26 27 28 29 30 31 32 41 fta1blem R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x W y = W
43 42 expr R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x W y = W
44 23 43 syl5bir R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W ¬ x = W y = W
45 44 orrd R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x = W y = W
46 45 ex R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x = W y = W
47 46 ralrimivva R CRing R NzRing f B 0 ˙ O f -1 W D f x Base R y Base R x R y = W x = W y = W
48 24 25 5 isdomn R Domn R NzRing x Base R y Base R x R y = W x = W y = W
49 22 47 48 sylanbrc R CRing R NzRing f B 0 ˙ O f -1 W D f R Domn
50 21 49 7 sylanbrc R CRing R NzRing f B 0 ˙ O f -1 W D f R IDomn
51 20 50 impbii R IDomn R CRing R NzRing f B 0 ˙ O f -1 W D f