Metamath Proof Explorer

Theorem ply1domn

Description: Corollary of deg1mul2 : the univariate polynomials over a domain are a domain. This is true for multivariate but with a much more complicated proof. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypothesis ply1domn.p 
|- P = ( Poly1 ` R )
Assertion ply1domn 
|- ( R e. Domn -> P e. Domn )

Proof

Step Hyp Ref Expression
1 ply1domn.p 
 |-  P = ( Poly1 ` R )
2 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
3 1 ply1nz 
 |-  ( R e. NzRing -> P e. NzRing )
4 2 3 syl 
 |-  ( R e. Domn -> P e. NzRing )
5 neanior 
 |-  ( ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) <-> -. ( x = ( 0g ` P ) \/ y = ( 0g ` P ) ) )
6 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
7 eqid 
 |-  ( RLReg ` R ) = ( RLReg ` R )
8 eqid 
 |-  ( Base ` P ) = ( Base ` P )
9 eqid 
 |-  ( .r ` P ) = ( .r ` P )
10 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
11 domnring 
 |-  ( R e. Domn -> R e. Ring )
12 11 ad2antrr 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> R e. Ring )
13 simplrl 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> x e. ( Base ` P ) )
14 simprl 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> x =/= ( 0g ` P ) )
15 simpll 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> R e. Domn )
16 eqid 
 |-  ( coe1 ` x ) = ( coe1 ` x )
17 6 1 10 8 7 16 deg1ldgdomn 
 |-  ( ( R e. Domn /\ x e. ( Base ` P ) /\ x =/= ( 0g ` P ) ) -> ( ( coe1 ` x ) ` ( ( deg1 ` R ) ` x ) ) e. ( RLReg ` R ) )
18 15 13 14 17 syl3anc 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> ( ( coe1 ` x ) ` ( ( deg1 ` R ) ` x ) ) e. ( RLReg ` R ) )
19 simplrr 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> y e. ( Base ` P ) )
20 simprr 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> y =/= ( 0g ` P ) )
21 6 1 7 8 9 10 12 13 14 18 19 20 deg1mul2 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> ( ( deg1 ` R ) ` ( x ( .r ` P ) y ) ) = ( ( ( deg1 ` R ) ` x ) + ( ( deg1 ` R ) ` y ) ) )
22 6 1 10 8 deg1nn0cl 
 |-  ( ( R e. Ring /\ x e. ( Base ` P ) /\ x =/= ( 0g ` P ) ) -> ( ( deg1 ` R ) ` x ) e. NN0 )
23 12 13 14 22 syl3anc 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> ( ( deg1 ` R ) ` x ) e. NN0 )
24 6 1 10 8 deg1nn0cl 
 |-  ( ( R e. Ring /\ y e. ( Base ` P ) /\ y =/= ( 0g ` P ) ) -> ( ( deg1 ` R ) ` y ) e. NN0 )
25 12 19 20 24 syl3anc 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> ( ( deg1 ` R ) ` y ) e. NN0 )
26 23 25 nn0addcld 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> ( ( ( deg1 ` R ) ` x ) + ( ( deg1 ` R ) ` y ) ) e. NN0 )
27 21 26 eqeltrd 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> ( ( deg1 ` R ) ` ( x ( .r ` P ) y ) ) e. NN0 )
28 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
29 11 28 syl 
 |-  ( R e. Domn -> P e. Ring )
30 29 ad2antrr 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> P e. Ring )
31 8 9 ringcl 
 |-  ( ( P e. Ring /\ x e. ( Base ` P ) /\ y e. ( Base ` P ) ) -> ( x ( .r ` P ) y ) e. ( Base ` P ) )
32 30 13 19 31 syl3anc 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> ( x ( .r ` P ) y ) e. ( Base ` P ) )
33 6 1 10 8 deg1nn0clb 
 |-  ( ( R e. Ring /\ ( x ( .r ` P ) y ) e. ( Base ` P ) ) -> ( ( x ( .r ` P ) y ) =/= ( 0g ` P ) <-> ( ( deg1 ` R ) ` ( x ( .r ` P ) y ) ) e. NN0 ) )
34 12 32 33 syl2anc 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> ( ( x ( .r ` P ) y ) =/= ( 0g ` P ) <-> ( ( deg1 ` R ) ` ( x ( .r ` P ) y ) ) e. NN0 ) )
35 27 34 mpbird 
 |-  ( ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) /\ ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) ) -> ( x ( .r ` P ) y ) =/= ( 0g ` P ) )
36 35 ex 
 |-  ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( ( x =/= ( 0g ` P ) /\ y =/= ( 0g ` P ) ) -> ( x ( .r ` P ) y ) =/= ( 0g ` P ) ) )
37 5 36 syl5bir 
 |-  ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( -. ( x = ( 0g ` P ) \/ y = ( 0g ` P ) ) -> ( x ( .r ` P ) y ) =/= ( 0g ` P ) ) )
38 37 necon4bd 
 |-  ( ( R e. Domn /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( ( x ( .r ` P ) y ) = ( 0g ` P ) -> ( x = ( 0g ` P ) \/ y = ( 0g ` P ) ) ) )
39 38 ralrimivva 
 |-  ( R e. Domn -> A. x e. ( Base ` P ) A. y e. ( Base ` P ) ( ( x ( .r ` P ) y ) = ( 0g ` P ) -> ( x = ( 0g ` P ) \/ y = ( 0g ` P ) ) ) )
40 8 9 10 isdomn 
 |-  ( P e. Domn <-> ( P e. NzRing /\ A. x e. ( Base ` P ) A. y e. ( Base ` P ) ( ( x ( .r ` P ) y ) = ( 0g ` P ) -> ( x = ( 0g ` P ) \/ y = ( 0g ` P ) ) ) ) )
41 4 39 40 sylanbrc 
 |-  ( R e. Domn -> P e. Domn )