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 ) |