MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ply1remlem Structured version   Unicode version

Theorem ply1remlem 21519
Description: A term of the form  x  -  N is linear, monic, and has exactly one zero. (Contributed by Mario Carneiro, 12-Jun-2015.)
Hypotheses
Ref Expression
ply1rem.p  |-  P  =  (Poly1 `  R )
ply1rem.b  |-  B  =  ( Base `  P
)
ply1rem.k  |-  K  =  ( Base `  R
)
ply1rem.x  |-  X  =  (var1 `  R )
ply1rem.m  |-  .-  =  ( -g `  P )
ply1rem.a  |-  A  =  (algSc `  P )
ply1rem.g  |-  G  =  ( X  .-  ( A `  N )
)
ply1rem.o  |-  O  =  (eval1 `  R )
ply1rem.1  |-  ( ph  ->  R  e. NzRing )
ply1rem.2  |-  ( ph  ->  R  e.  CRing )
ply1rem.3  |-  ( ph  ->  N  e.  K )
ply1rem.u  |-  U  =  (Monic1p `  R )
ply1rem.d  |-  D  =  ( deg1  `  R )
ply1rem.z  |-  .0.  =  ( 0g `  R )
Assertion
Ref Expression
ply1remlem  |-  ( ph  ->  ( G  e.  U  /\  ( D `  G
)  =  1  /\  ( `' ( O `
 G ) " {  .0.  } )  =  { N } ) )

Proof of Theorem ply1remlem
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 ply1rem.g . . . 4  |-  G  =  ( X  .-  ( A `  N )
)
2 ply1rem.1 . . . . . . . 8  |-  ( ph  ->  R  e. NzRing )
3 nzrrng 17265 . . . . . . . 8  |-  ( R  e. NzRing  ->  R  e.  Ring )
42, 3syl 16 . . . . . . 7  |-  ( ph  ->  R  e.  Ring )
5 ply1rem.p . . . . . . . 8  |-  P  =  (Poly1 `  R )
65ply1rng 17601 . . . . . . 7  |-  ( R  e.  Ring  ->  P  e. 
Ring )
74, 6syl 16 . . . . . 6  |-  ( ph  ->  P  e.  Ring )
8 rnggrp 16586 . . . . . 6  |-  ( P  e.  Ring  ->  P  e. 
Grp )
97, 8syl 16 . . . . 5  |-  ( ph  ->  P  e.  Grp )
10 ply1rem.x . . . . . . 7  |-  X  =  (var1 `  R )
11 ply1rem.b . . . . . . 7  |-  B  =  ( Base `  P
)
1210, 5, 11vr1cl 17570 . . . . . 6  |-  ( R  e.  Ring  ->  X  e.  B )
134, 12syl 16 . . . . 5  |-  ( ph  ->  X  e.  B )
14 ply1rem.a . . . . . . . 8  |-  A  =  (algSc `  P )
15 ply1rem.k . . . . . . . 8  |-  K  =  ( Base `  R
)
165, 14, 15, 11ply1sclf 17636 . . . . . . 7  |-  ( R  e.  Ring  ->  A : K
--> B )
174, 16syl 16 . . . . . 6  |-  ( ph  ->  A : K --> B )
18 ply1rem.3 . . . . . 6  |-  ( ph  ->  N  e.  K )
1917, 18ffvelrnd 5832 . . . . 5  |-  ( ph  ->  ( A `  N
)  e.  B )
20 ply1rem.m . . . . . 6  |-  .-  =  ( -g `  P )
2111, 20grpsubcl 15586 . . . . 5  |-  ( ( P  e.  Grp  /\  X  e.  B  /\  ( A `  N )  e.  B )  -> 
( X  .-  ( A `  N )
)  e.  B )
229, 13, 19, 21syl3anc 1211 . . . 4  |-  ( ph  ->  ( X  .-  ( A `  N )
)  e.  B )
231, 22syl5eqel 2517 . . 3  |-  ( ph  ->  G  e.  B )
241fveq2i 5682 . . . . . . 7  |-  ( D `
 G )  =  ( D `  ( X  .-  ( A `  N ) ) )
25 ply1rem.d . . . . . . . 8  |-  D  =  ( deg1  `  R )
2625, 5, 11deg1xrcl 21438 . . . . . . . . . . 11  |-  ( ( A `  N )  e.  B  ->  ( D `  ( A `  N ) )  e. 
RR* )
2719, 26syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( D `  ( A `  N )
)  e.  RR* )
28 0xr 9418 . . . . . . . . . . 11  |-  0  e.  RR*
2928a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  e.  RR* )
30 1re 9373 . . . . . . . . . . 11  |-  1  e.  RR
31 rexr 9417 . . . . . . . . . . 11  |-  ( 1  e.  RR  ->  1  e.  RR* )
3230, 31mp1i 12 . . . . . . . . . 10  |-  ( ph  ->  1  e.  RR* )
3325, 5, 15, 14deg1sclle 21469 . . . . . . . . . . 11  |-  ( ( R  e.  Ring  /\  N  e.  K )  ->  ( D `  ( A `  N ) )  <_ 
0 )
344, 18, 33syl2anc 654 . . . . . . . . . 10  |-  ( ph  ->  ( D `  ( A `  N )
)  <_  0 )
35 0lt1 9850 . . . . . . . . . . 11  |-  0  <  1
3635a1i 11 . . . . . . . . . 10  |-  ( ph  ->  0  <  1 )
3727, 29, 32, 34, 36xrlelttrd 11122 . . . . . . . . 9  |-  ( ph  ->  ( D `  ( A `  N )
)  <  1 )
38 eqid 2433 . . . . . . . . . . . . . 14  |-  (mulGrp `  P )  =  (mulGrp `  P )
3938, 11mgpbas 16571 . . . . . . . . . . . . 13  |-  B  =  ( Base `  (mulGrp `  P ) )
40 eqid 2433 . . . . . . . . . . . . 13  |-  (.g `  (mulGrp `  P ) )  =  (.g `  (mulGrp `  P
) )
4139, 40mulg1 15614 . . . . . . . . . . . 12  |-  ( X  e.  B  ->  (
1 (.g `  (mulGrp `  P
) ) X )  =  X )
4213, 41syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( 1 (.g `  (mulGrp `  P ) ) X )  =  X )
4342fveq2d 5683 . . . . . . . . . 10  |-  ( ph  ->  ( D `  (
1 (.g `  (mulGrp `  P
) ) X ) )  =  ( D `
 X ) )
44 1nn0 10583 . . . . . . . . . . 11  |-  1  e.  NN0
4525, 5, 10, 38, 40deg1pw 21477 . . . . . . . . . . 11  |-  ( ( R  e. NzRing  /\  1  e.  NN0 )  ->  ( D `  ( 1
(.g `  (mulGrp `  P
) ) X ) )  =  1 )
462, 44, 45sylancl 655 . . . . . . . . . 10  |-  ( ph  ->  ( D `  (
1 (.g `  (mulGrp `  P
) ) X ) )  =  1 )
4743, 46eqtr3d 2467 . . . . . . . . 9  |-  ( ph  ->  ( D `  X
)  =  1 )
4837, 47breqtrrd 4306 . . . . . . . 8  |-  ( ph  ->  ( D `  ( A `  N )
)  <  ( D `  X ) )
495, 25, 4, 11, 20, 13, 19, 48deg1sub 21465 . . . . . . 7  |-  ( ph  ->  ( D `  ( X  .-  ( A `  N ) ) )  =  ( D `  X ) )
5024, 49syl5eq 2477 . . . . . 6  |-  ( ph  ->  ( D `  G
)  =  ( D `
 X ) )
5150, 47eqtrd 2465 . . . . 5  |-  ( ph  ->  ( D `  G
)  =  1 )
5251, 44syl6eqel 2521 . . . 4  |-  ( ph  ->  ( D `  G
)  e.  NN0 )
53 eqid 2433 . . . . . 6  |-  ( 0g
`  P )  =  ( 0g `  P
)
5425, 5, 53, 11deg1nn0clb 21446 . . . . 5  |-  ( ( R  e.  Ring  /\  G  e.  B )  ->  ( G  =/=  ( 0g `  P )  <->  ( D `  G )  e.  NN0 ) )
554, 23, 54syl2anc 654 . . . 4  |-  ( ph  ->  ( G  =/=  ( 0g `  P )  <->  ( D `  G )  e.  NN0 ) )
5652, 55mpbird 232 . . 3  |-  ( ph  ->  G  =/=  ( 0g
`  P ) )
5751fveq2d 5683 . . . 4  |-  ( ph  ->  ( (coe1 `  G ) `  ( D `  G ) )  =  ( (coe1 `  G ) `  1
) )
581fveq2i 5682 . . . . . 6  |-  (coe1 `  G
)  =  (coe1 `  ( X  .-  ( A `  N ) ) )
5958fveq1i 5680 . . . . 5  |-  ( (coe1 `  G ) `  1
)  =  ( (coe1 `  ( X  .-  ( A `  N )
) ) `  1
)
6044a1i 11 . . . . . 6  |-  ( ph  ->  1  e.  NN0 )
61 eqid 2433 . . . . . . 7  |-  ( -g `  R )  =  (
-g `  R )
625, 11, 20, 61coe1subfv 17618 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  X  e.  B  /\  ( A `  N )  e.  B )  /\  1  e.  NN0 )  -> 
( (coe1 `  ( X  .-  ( A `  N ) ) ) `  1
)  =  ( ( (coe1 `  X ) ` 
1 ) ( -g `  R ) ( (coe1 `  ( A `  N
) ) `  1
) ) )
634, 13, 19, 60, 62syl31anc 1214 . . . . 5  |-  ( ph  ->  ( (coe1 `  ( X  .-  ( A `  N ) ) ) `  1
)  =  ( ( (coe1 `  X ) ` 
1 ) ( -g `  R ) ( (coe1 `  ( A `  N
) ) `  1
) ) )
6459, 63syl5eq 2477 . . . 4  |-  ( ph  ->  ( (coe1 `  G ) ` 
1 )  =  ( ( (coe1 `  X ) ` 
1 ) ( -g `  R ) ( (coe1 `  ( A `  N
) ) `  1
) ) )
6542oveq2d 6096 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1r `  R ) ( .s
`  P ) ( 1 (.g `  (mulGrp `  P
) ) X ) )  =  ( ( 1r `  R ) ( .s `  P
) X ) )
665ply1sca 17606 . . . . . . . . . . . . 13  |-  ( R  e. NzRing  ->  R  =  (Scalar `  P ) )
672, 66syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  R  =  (Scalar `  P ) )
6867fveq2d 5683 . . . . . . . . . . 11  |-  ( ph  ->  ( 1r `  R
)  =  ( 1r
`  (Scalar `  P )
) )
6968oveq1d 6095 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1r `  R ) ( .s
`  P ) X )  =  ( ( 1r `  (Scalar `  P ) ) ( .s `  P ) X ) )
705ply1lmod 17605 . . . . . . . . . . . 12  |-  ( R  e.  Ring  ->  P  e. 
LMod )
714, 70syl 16 . . . . . . . . . . 11  |-  ( ph  ->  P  e.  LMod )
72 eqid 2433 . . . . . . . . . . . 12  |-  (Scalar `  P )  =  (Scalar `  P )
73 eqid 2433 . . . . . . . . . . . 12  |-  ( .s
`  P )  =  ( .s `  P
)
74 eqid 2433 . . . . . . . . . . . 12  |-  ( 1r
`  (Scalar `  P )
)  =  ( 1r
`  (Scalar `  P )
)
7511, 72, 73, 74lmodvs1 16900 . . . . . . . . . . 11  |-  ( ( P  e.  LMod  /\  X  e.  B )  ->  (
( 1r `  (Scalar `  P ) ) ( .s `  P ) X )  =  X )
7671, 13, 75syl2anc 654 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1r `  (Scalar `  P ) ) ( .s `  P
) X )  =  X )
7765, 69, 763eqtrd 2469 . . . . . . . . 9  |-  ( ph  ->  ( ( 1r `  R ) ( .s
`  P ) ( 1 (.g `  (mulGrp `  P
) ) X ) )  =  X )
7877fveq2d 5683 . . . . . . . 8  |-  ( ph  ->  (coe1 `  ( ( 1r
`  R ) ( .s `  P ) ( 1 (.g `  (mulGrp `  P ) ) X ) ) )  =  (coe1 `  X ) )
7978fveq1d 5681 . . . . . . 7  |-  ( ph  ->  ( (coe1 `  ( ( 1r
`  R ) ( .s `  P ) ( 1 (.g `  (mulGrp `  P ) ) X ) ) ) ` 
1 )  =  ( (coe1 `  X ) ` 
1 ) )
80 eqid 2433 . . . . . . . . . 10  |-  ( 1r
`  R )  =  ( 1r `  R
)
8115, 80rngidcl 16601 . . . . . . . . 9  |-  ( R  e.  Ring  ->  ( 1r
`  R )  e.  K )
824, 81syl 16 . . . . . . . 8  |-  ( ph  ->  ( 1r `  R
)  e.  K )
83 ply1rem.z . . . . . . . . 9  |-  .0.  =  ( 0g `  R )
8483, 15, 5, 10, 73, 38, 40coe1tmfv1 17625 . . . . . . . 8  |-  ( ( R  e.  Ring  /\  ( 1r `  R )  e.  K  /\  1  e. 
NN0 )  ->  (
(coe1 `  ( ( 1r
`  R ) ( .s `  P ) ( 1 (.g `  (mulGrp `  P ) ) X ) ) ) ` 
1 )  =  ( 1r `  R ) )
854, 82, 60, 84syl3anc 1211 . . . . . . 7  |-  ( ph  ->  ( (coe1 `  ( ( 1r
`  R ) ( .s `  P ) ( 1 (.g `  (mulGrp `  P ) ) X ) ) ) ` 
1 )  =  ( 1r `  R ) )
8679, 85eqtr3d 2467 . . . . . 6  |-  ( ph  ->  ( (coe1 `  X ) ` 
1 )  =  ( 1r `  R ) )
87 eqid 2433 . . . . . . . . . 10  |-  ( 0g
`  R )  =  ( 0g `  R
)
885, 14, 15, 87coe1scl 17637 . . . . . . . . 9  |-  ( ( R  e.  Ring  /\  N  e.  K )  ->  (coe1 `  ( A `  N ) )  =  ( x  e.  NN0  |->  if ( x  =  0 ,  N ,  ( 0g
`  R ) ) ) )
894, 18, 88syl2anc 654 . . . . . . . 8  |-  ( ph  ->  (coe1 `  ( A `  N ) )  =  ( x  e.  NN0  |->  if ( x  =  0 ,  N ,  ( 0g `  R ) ) ) )
9089fveq1d 5681 . . . . . . 7  |-  ( ph  ->  ( (coe1 `  ( A `  N ) ) ` 
1 )  =  ( ( x  e.  NN0  |->  if ( x  =  0 ,  N ,  ( 0g `  R ) ) ) `  1
) )
91 ax-1ne0 9339 . . . . . . . . . . 11  |-  1  =/=  0
92 neeq1 2606 . . . . . . . . . . 11  |-  ( x  =  1  ->  (
x  =/=  0  <->  1  =/=  0 ) )
9391, 92mpbiri 233 . . . . . . . . . 10  |-  ( x  =  1  ->  x  =/=  0 )
94 ifnefalse 3789 . . . . . . . . . 10  |-  ( x  =/=  0  ->  if ( x  =  0 ,  N ,  ( 0g
`  R ) )  =  ( 0g `  R ) )
9593, 94syl 16 . . . . . . . . 9  |-  ( x  =  1  ->  if ( x  =  0 ,  N ,  ( 0g
`  R ) )  =  ( 0g `  R ) )
96 eqid 2433 . . . . . . . . 9  |-  ( x  e.  NN0  |->  if ( x  =  0 ,  N ,  ( 0g
`  R ) ) )  =  ( x  e.  NN0  |->  if ( x  =  0 ,  N ,  ( 0g
`  R ) ) )
97 fvex 5689 . . . . . . . . 9  |-  ( 0g
`  R )  e. 
_V
9895, 96, 97fvmpt 5762 . . . . . . . 8  |-  ( 1  e.  NN0  ->  ( ( x  e.  NN0  |->  if ( x  =  0 ,  N ,  ( 0g
`  R ) ) ) `  1 )  =  ( 0g `  R ) )
9944, 98ax-mp 5 . . . . . . 7  |-  ( ( x  e.  NN0  |->  if ( x  =  0 ,  N ,  ( 0g
`  R ) ) ) `  1 )  =  ( 0g `  R )
10090, 99syl6eq 2481 . . . . . 6  |-  ( ph  ->  ( (coe1 `  ( A `  N ) ) ` 
1 )  =  ( 0g `  R ) )
10186, 100oveq12d 6098 . . . . 5  |-  ( ph  ->  ( ( (coe1 `  X
) `  1 )
( -g `  R ) ( (coe1 `  ( A `  N ) ) ` 
1 ) )  =  ( ( 1r `  R ) ( -g `  R ) ( 0g
`  R ) ) )
102 rnggrp 16586 . . . . . . 7  |-  ( R  e.  Ring  ->  R  e. 
Grp )
1034, 102syl 16 . . . . . 6  |-  ( ph  ->  R  e.  Grp )
10415, 87, 61grpsubid1 15591 . . . . . 6  |-  ( ( R  e.  Grp  /\  ( 1r `  R )  e.  K )  -> 
( ( 1r `  R ) ( -g `  R ) ( 0g
`  R ) )  =  ( 1r `  R ) )
105103, 82, 104syl2anc 654 . . . . 5  |-  ( ph  ->  ( ( 1r `  R ) ( -g `  R ) ( 0g
`  R ) )  =  ( 1r `  R ) )
106101, 105eqtrd 2465 . . . 4  |-  ( ph  ->  ( ( (coe1 `  X
) `  1 )
( -g `  R ) ( (coe1 `  ( A `  N ) ) ` 
1 ) )  =  ( 1r `  R
) )
10757, 64, 1063eqtrd 2469 . . 3  |-  ( ph  ->  ( (coe1 `  G ) `  ( D `  G ) )  =  ( 1r
`  R ) )
108 ply1rem.u . . . 4  |-  U  =  (Monic1p `  R )
1095, 11, 53, 25, 108, 80ismon1p 21499 . . 3  |-  ( G  e.  U  <->  ( G  e.  B  /\  G  =/=  ( 0g `  P
)  /\  ( (coe1 `  G ) `  ( D `  G )
)  =  ( 1r
`  R ) ) )
11023, 56, 107, 109syl3anbrc 1165 . 2  |-  ( ph  ->  G  e.  U )
1111fveq2i 5682 . . . . . . . . . 10  |-  ( O `
 G )  =  ( O `  ( X  .-  ( A `  N ) ) )
112111fveq1i 5680 . . . . . . . . 9  |-  ( ( O `  G ) `
 x )  =  ( ( O `  ( X  .-  ( A `
 N ) ) ) `  x )
113 ply1rem.o . . . . . . . . . . 11  |-  O  =  (eval1 `  R )
114 ply1rem.2 . . . . . . . . . . . 12  |-  ( ph  ->  R  e.  CRing )
115114adantr 462 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  K )  ->  R  e.  CRing )
116 simpr 458 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  K )  ->  x  e.  K )
117113, 10, 15, 5, 11, 115, 116evl1vard 21384 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  K )  ->  ( X  e.  B  /\  ( ( O `  X ) `  x
)  =  x ) )
11818adantr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  K )  ->  N  e.  K )
119113, 5, 15, 14, 11, 115, 118, 116evl1scad 21382 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  K )  ->  (
( A `  N
)  e.  B  /\  ( ( O `  ( A `  N ) ) `  x )  =  N ) )
120113, 5, 15, 11, 115, 116, 117, 119, 20, 61evl1subd 21386 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  K )  ->  (
( X  .-  ( A `  N )
)  e.  B  /\  ( ( O `  ( X  .-  ( A `
 N ) ) ) `  x )  =  ( x (
-g `  R ) N ) ) )
121120simprd 460 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  K )  ->  (
( O `  ( X  .-  ( A `  N ) ) ) `
 x )  =  ( x ( -g `  R ) N ) )
122112, 121syl5eq 2477 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  (
( O `  G
) `  x )  =  ( x (
-g `  R ) N ) )
123122eqeq1d 2441 . . . . . . 7  |-  ( (
ph  /\  x  e.  K )  ->  (
( ( O `  G ) `  x
)  =  .0.  <->  ( x
( -g `  R ) N )  =  .0.  ) )
124103adantr 462 . . . . . . . 8  |-  ( (
ph  /\  x  e.  K )  ->  R  e.  Grp )
12515, 83, 61grpsubeq0 15592 . . . . . . . 8  |-  ( ( R  e.  Grp  /\  x  e.  K  /\  N  e.  K )  ->  ( ( x (
-g `  R ) N )  =  .0.  <->  x  =  N ) )
126124, 116, 118, 125syl3anc 1211 . . . . . . 7  |-  ( (
ph  /\  x  e.  K )  ->  (
( x ( -g `  R ) N )  =  .0.  <->  x  =  N ) )
127123, 126bitrd 253 . . . . . 6  |-  ( (
ph  /\  x  e.  K )  ->  (
( ( O `  G ) `  x
)  =  .0.  <->  x  =  N ) )
128 elsn 3879 . . . . . 6  |-  ( x  e.  { N }  <->  x  =  N )
129127, 128syl6bbr 263 . . . . 5  |-  ( (
ph  /\  x  e.  K )  ->  (
( ( O `  G ) `  x
)  =  .0.  <->  x  e.  { N } ) )
130129pm5.32da 634 . . . 4  |-  ( ph  ->  ( ( x  e.  K  /\  ( ( O `  G ) `
 x )  =  .0.  )  <->  ( x  e.  K  /\  x  e.  { N } ) ) )
131 eqid 2433 . . . . . . 7  |-  ( R  ^s  K )  =  ( R  ^s  K )
132 eqid 2433 . . . . . . 7  |-  ( Base `  ( R  ^s  K ) )  =  ( Base `  ( R  ^s  K ) )
133 fvex 5689 . . . . . . . . 9  |-  ( Base `  R )  e.  _V
13415, 133eqeltri 2503 . . . . . . . 8  |-  K  e. 
_V
135134a1i 11 . . . . . . 7  |-  ( ph  ->  K  e.  _V )
136113, 5, 131, 15evl1rhm 21380 . . . . . . . . . 10  |-  ( R  e.  CRing  ->  O  e.  ( P RingHom  ( R  ^s  K
) ) )
137114, 136syl 16 . . . . . . . . 9  |-  ( ph  ->  O  e.  ( P RingHom 
( R  ^s  K ) ) )
13811, 132rhmf 16748 . . . . . . . . 9  |-  ( O  e.  ( P RingHom  ( R  ^s  K ) )  ->  O : B --> ( Base `  ( R  ^s  K ) ) )
139137, 138syl 16 . . . . . . . 8  |-  ( ph  ->  O : B --> ( Base `  ( R  ^s  K ) ) )
140139, 23ffvelrnd 5832 . . . . . . 7  |-  ( ph  ->  ( O `  G
)  e.  ( Base `  ( R  ^s  K ) ) )
141131, 15, 132, 2, 135, 140pwselbas 14410 . . . . . 6  |-  ( ph  ->  ( O `  G
) : K --> K )
142 ffn 5547 . . . . . 6  |-  ( ( O `  G ) : K --> K  -> 
( O `  G
)  Fn  K )
143141, 142syl 16 . . . . 5  |-  ( ph  ->  ( O `  G
)  Fn  K )
144 fniniseg 5812 . . . . 5  |-  ( ( O `  G )  Fn  K  ->  (
x  e.  ( `' ( O `  G
) " {  .0.  } )  <->  ( x  e.  K  /\  ( ( O `  G ) `
 x )  =  .0.  ) ) )
145143, 144syl 16 . . . 4  |-  ( ph  ->  ( x  e.  ( `' ( O `  G ) " {  .0.  } )  <->  ( x  e.  K  /\  (
( O `  G
) `  x )  =  .0.  ) ) )
14618snssd 4006 . . . . . 6  |-  ( ph  ->  { N }  C_  K )
147146sseld 3343 . . . . 5  |-  ( ph  ->  ( x  e.  { N }  ->  x  e.  K ) )
148147pm4.71rd 628 . . . 4  |-  ( ph  ->  ( x  e.  { N }  <->  ( x  e.  K  /\  x  e. 
{ N } ) ) )
149130, 145, 1483bitr4d 285 . . 3  |-  ( ph  ->  ( x  e.  ( `' ( O `  G ) " {  .0.  } )  <->  x  e.  { N } ) )
150149eqrdv 2431 . 2  |-  ( ph  ->  ( `' ( O `
 G ) " {  .0.  } )  =  { N } )
151110, 51, 1503jca 1161 1  |-  ( ph  ->  ( G  e.  U  /\  ( D `  G
)  =  1  /\  ( `' ( O `
 G ) " {  .0.  } )  =  { N } ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 958    = wceq 1362    e. wcel 1755    =/= wne 2596   _Vcvv 2962   ifcif 3779   {csn 3865   class class class wbr 4280    e. cmpt 4338   `'ccnv 4826   "cima 4830    Fn wfn 5401   -->wf 5402   ` cfv 5406  (class class class)co 6080   RRcr 9269   0cc0 9270   1c1 9271   RR*cxr 9405    < clt 9406    <_ cle 9407   NN0cn0 10567   Basecbs 14157  Scalarcsca 14224   .scvsca 14225   0gc0g 14361    ^s cpws 14368   Grpcgrp 15393   -gcsg 15396  .gcmg 15397  mulGrpcmgp 16565   Ringcrg 16577   CRingccrg 16578   1rcur 16579   RingHom crh 16738   LModclmod 16872  NzRingcnzr 17261  algSccascl 17305  var1cv1 17527  Poly1cpl1 17528  eval1ce1 17530  coe1cco1 17531   deg1 cdg1 21408  Monic1pcmn1 21482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-inf2 7835  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347  ax-pre-sup 9348  ax-addf 9349  ax-mulf 9350
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-iin 4162  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-se 4667  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-isom 5415  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-of 6309  df-ofr 6310  df-om 6466  df-1st 6566  df-2nd 6567  df-supp 6680  df-tpos 6734  df-recs 6818  df-rdg 6852  df-1o 6908  df-2o 6909  df-oadd 6912  df-er 7089  df-map 7204  df-pm 7205  df-ixp 7252  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-fsupp 7609  df-sup 7679  df-oi 7712  df-card 8097  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-nn 10311  df-2 10368  df-3 10369  df-4 10370  df-5 10371  df-6 10372  df-7 10373  df-8 10374  df-9 10375  df-10 10376  df-n0 10568  df-z 10635  df-dec 10744  df-uz 10850  df-fz 11425  df-fzo 11533  df-seq 11791  df-hash 12088  df-struct 14159  df-ndx 14160  df-slot 14161  df-base 14162  df-sets 14163  df-ress 14164  df-plusg 14234  df-mulr 14235  df-starv 14236  df-sca 14237  df-vsca 14238  df-ip 14239  df-tset 14240  df-ple 14241  df-ds 14243  df-unif 14244  df-hom 14245  df-cco 14246  df-0g 14363  df-gsum 14364  df-prds 14369  df-pws 14371  df-mre 14507  df-mrc 14508  df-acs 14510  df-mnd 15398  df-mhm 15447  df-submnd 15448  df-grp 15525  df-minusg 15526  df-sbg 15527  df-mulg 15528  df-subg 15658  df-ghm 15725  df-cntz 15815  df-cmn 16259  df-abl 16260  df-mgp 16566  df-rng 16580  df-cring 16581  df-ur 16582  df-oppr 16649  df-dvdsr 16667  df-unit 16668  df-invr 16698  df-rnghom 16740  df-subrg 16787  df-lmod 16874  df-lss 16936  df-lsp 16975  df-nzr 17262  df-rlreg 17276  df-assa 17306  df-asp 17307  df-ascl 17308  df-psr 17351  df-mvr 17352  df-mpl 17353  df-evls 17354  df-evl 17355  df-opsr 17359  df-psr1 17533  df-vr1 17534  df-ply1 17535  df-evl1 17537  df-coe1 17538  df-cnfld 17663  df-mdeg 21409  df-deg1 21410  df-mon1 21487
This theorem is referenced by:  ply1rem  21520  facth1  21521  fta1glem1  21522  fta1glem2  21523
  Copyright terms: Public domain W3C validator