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

Theorem ig1pdvds 20104
Description: The monic generator of an ideal divides all elements of the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.)
Hypotheses
Ref Expression
ig1pval.p  |-  P  =  (Poly1 `  R )
ig1pval.g  |-  G  =  (idlGen1p `
 R )
ig1pcl.u  |-  U  =  (LIdeal `  P )
ig1pdvds.d  |-  .||  =  (
||r `  P )
Assertion
Ref Expression
ig1pdvds  |-  ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  ->  ( G `  I )  .|| 
X )

Proof of Theorem ig1pdvds
StepHypRef Expression
1 drngrng 15847 . . . . . . 7  |-  ( R  e.  DivRing  ->  R  e.  Ring )
2 ig1pval.p . . . . . . . 8  |-  P  =  (Poly1 `  R )
32ply1rng 16647 . . . . . . 7  |-  ( R  e.  Ring  ->  P  e. 
Ring )
41, 3syl 16 . . . . . 6  |-  ( R  e.  DivRing  ->  P  e.  Ring )
543ad2ant1 979 . . . . 5  |-  ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  ->  P  e.  Ring )
6 eqid 2438 . . . . . . . 8  |-  ( Base `  P )  =  (
Base `  P )
7 ig1pcl.u . . . . . . . 8  |-  U  =  (LIdeal `  P )
86, 7lidlss 16285 . . . . . . 7  |-  ( I  e.  U  ->  I  C_  ( Base `  P
) )
983ad2ant2 980 . . . . . 6  |-  ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  ->  I  C_  ( Base `  P
) )
10 ig1pval.g . . . . . . . 8  |-  G  =  (idlGen1p `
 R )
112, 10, 7ig1pcl 20103 . . . . . . 7  |-  ( ( R  e.  DivRing  /\  I  e.  U )  ->  ( G `  I )  e.  I )
12113adant3 978 . . . . . 6  |-  ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  ->  ( G `  I )  e.  I )
139, 12sseldd 3351 . . . . 5  |-  ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  ->  ( G `  I )  e.  ( Base `  P
) )
14 ig1pdvds.d . . . . . 6  |-  .||  =  (
||r `  P )
15 eqid 2438 . . . . . 6  |-  ( 0g
`  P )  =  ( 0g `  P
)
166, 14, 15dvdsr01 15765 . . . . 5  |-  ( ( P  e.  Ring  /\  ( G `  I )  e.  ( Base `  P
) )  ->  ( G `  I )  .||  ( 0g `  P
) )
175, 13, 16syl2anc 644 . . . 4  |-  ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  ->  ( G `  I )  .||  ( 0g `  P
) )
1817adantr 453 . . 3  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =  {
( 0g `  P
) } )  -> 
( G `  I
)  .||  ( 0g `  P ) )
19 eleq2 2499 . . . . . 6  |-  ( I  =  { ( 0g
`  P ) }  ->  ( X  e.  I  <->  X  e.  { ( 0g `  P ) } ) )
2019biimpac 474 . . . . 5  |-  ( ( X  e.  I  /\  I  =  { ( 0g `  P ) } )  ->  X  e.  { ( 0g `  P
) } )
21203ad2antl3 1122 . . . 4  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =  {
( 0g `  P
) } )  ->  X  e.  { ( 0g `  P ) } )
22 elsni 3840 . . . 4  |-  ( X  e.  { ( 0g
`  P ) }  ->  X  =  ( 0g `  P ) )
2321, 22syl 16 . . 3  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =  {
( 0g `  P
) } )  ->  X  =  ( 0g `  P ) )
2418, 23breqtrrd 4241 . 2  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =  {
( 0g `  P
) } )  -> 
( G `  I
)  .||  X )
25 simpl1 961 . . . . . . . 8  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  R  e.  DivRing )
2625, 1syl 16 . . . . . . 7  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  R  e.  Ring )
27 simpl2 962 . . . . . . . . 9  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  I  e.  U )
2827, 8syl 16 . . . . . . . 8  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  I  C_  ( Base `  P
) )
29 simpl3 963 . . . . . . . 8  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  X  e.  I )
3028, 29sseldd 3351 . . . . . . 7  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  X  e.  ( Base `  P
) )
31 simpr 449 . . . . . . . . . 10  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  I  =/=  { ( 0g `  P ) } )
32 eqid 2438 . . . . . . . . . . 11  |-  ( deg1  `  R
)  =  ( deg1  `  R
)
33 eqid 2438 . . . . . . . . . . 11  |-  (Monic1p `  R
)  =  (Monic1p `  R
)
342, 10, 15, 7, 32, 33ig1pval3 20102 . . . . . . . . . 10  |-  ( ( R  e.  DivRing  /\  I  e.  U  /\  I  =/= 
{ ( 0g `  P ) } )  ->  ( ( G `
 I )  e.  I  /\  ( G `
 I )  e.  (Monic1p `  R )  /\  ( ( deg1  `  R ) `  ( G `  I
) )  =  sup ( ( ( deg1  `  R
) " ( I 
\  { ( 0g
`  P ) } ) ) ,  RR ,  `'  <  ) ) )
3525, 27, 31, 34syl3anc 1185 . . . . . . . . 9  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( G `  I
)  e.  I  /\  ( G `  I )  e.  (Monic1p `  R )  /\  ( ( deg1  `  R ) `  ( G `  I
) )  =  sup ( ( ( deg1  `  R
) " ( I 
\  { ( 0g
`  P ) } ) ) ,  RR ,  `'  <  ) ) )
3635simp2d 971 . . . . . . . 8  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( G `  I )  e.  (Monic1p `  R ) )
37 eqid 2438 . . . . . . . . 9  |-  (Unic1p `  R
)  =  (Unic1p `  R
)
3837, 33mon1puc1p 20078 . . . . . . . 8  |-  ( ( R  e.  Ring  /\  ( G `  I )  e.  (Monic1p `  R ) )  ->  ( G `  I )  e.  (Unic1p `  R ) )
3926, 36, 38syl2anc 644 . . . . . . 7  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( G `  I )  e.  (Unic1p `  R ) )
40 eqid 2438 . . . . . . . 8  |-  (rem1p `  R
)  =  (rem1p `  R
)
4140, 2, 6, 37, 32r1pdeglt 20086 . . . . . . 7  |-  ( ( R  e.  Ring  /\  X  e.  ( Base `  P
)  /\  ( G `  I )  e.  (Unic1p `  R ) )  -> 
( ( deg1  `  R ) `  ( X (rem1p `  R
) ( G `  I ) ) )  <  ( ( deg1  `  R
) `  ( G `  I ) ) )
4226, 30, 39, 41syl3anc 1185 . . . . . 6  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( deg1  `
 R ) `  ( X (rem1p `  R ) ( G `  I ) ) )  <  (
( deg1  `
 R ) `  ( G `  I ) ) )
4335simp3d 972 . . . . . 6  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( deg1  `
 R ) `  ( G `  I ) )  =  sup (
( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) ) ,  RR ,  `'  <  ) )
4442, 43breqtrd 4239 . . . . 5  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( deg1  `
 R ) `  ( X (rem1p `  R ) ( G `  I ) ) )  <  sup ( ( ( deg1  `  R
) " ( I 
\  { ( 0g
`  P ) } ) ) ,  RR ,  `'  <  ) )
4532, 2, 6deg1xrf 20009 . . . . . . 7  |-  ( deg1  `  R
) : ( Base `  P ) --> RR*
4635simp1d 970 . . . . . . . . . . 11  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( G `  I )  e.  I )
4728, 46sseldd 3351 . . . . . . . . . 10  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( G `  I )  e.  ( Base `  P
) )
48 eqid 2438 . . . . . . . . . . 11  |-  (quot1p `  R
)  =  (quot1p `  R
)
49 eqid 2438 . . . . . . . . . . 11  |-  ( .r
`  P )  =  ( .r `  P
)
50 eqid 2438 . . . . . . . . . . 11  |-  ( -g `  P )  =  (
-g `  P )
5140, 2, 6, 48, 49, 50r1pval 20084 . . . . . . . . . 10  |-  ( ( X  e.  ( Base `  P )  /\  ( G `  I )  e.  ( Base `  P
) )  ->  ( X (rem1p `  R ) ( G `  I ) )  =  ( X ( -g `  P
) ( ( X (quot1p `  R ) ( G `  I ) ) ( .r `  P ) ( G `
 I ) ) ) )
5230, 47, 51syl2anc 644 . . . . . . . . 9  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( X (rem1p `  R ) ( G `  I ) )  =  ( X ( -g `  P
) ( ( X (quot1p `  R ) ( G `  I ) ) ( .r `  P ) ( G `
 I ) ) ) )
5326, 3syl 16 . . . . . . . . . 10  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  P  e.  Ring )
5448, 2, 6, 37q1pcl 20083 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  X  e.  ( Base `  P
)  /\  ( G `  I )  e.  (Unic1p `  R ) )  -> 
( X (quot1p `  R
) ( G `  I ) )  e.  ( Base `  P
) )
5526, 30, 39, 54syl3anc 1185 . . . . . . . . . . 11  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( X (quot1p `  R ) ( G `  I ) )  e.  ( Base `  P ) )
567, 6, 49lidlmcl 16293 . . . . . . . . . . 11  |-  ( ( ( P  e.  Ring  /\  I  e.  U )  /\  ( ( X (quot1p `  R ) ( G `  I ) )  e.  ( Base `  P )  /\  ( G `  I )  e.  I ) )  -> 
( ( X (quot1p `  R ) ( G `
 I ) ) ( .r `  P
) ( G `  I ) )  e.  I )
5753, 27, 55, 46, 56syl22anc 1186 . . . . . . . . . 10  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( X (quot1p `  R
) ( G `  I ) ) ( .r `  P ) ( G `  I
) )  e.  I
)
587, 50lidlsubcl 16292 . . . . . . . . . 10  |-  ( ( ( P  e.  Ring  /\  I  e.  U )  /\  ( X  e.  I  /\  ( ( X (quot1p `  R ) ( G `  I ) ) ( .r `  P ) ( G `
 I ) )  e.  I ) )  ->  ( X (
-g `  P )
( ( X (quot1p `  R ) ( G `
 I ) ) ( .r `  P
) ( G `  I ) ) )  e.  I )
5953, 27, 29, 57, 58syl22anc 1186 . . . . . . . . 9  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( X ( -g `  P
) ( ( X (quot1p `  R ) ( G `  I ) ) ( .r `  P ) ( G `
 I ) ) )  e.  I )
6052, 59eqeltrd 2512 . . . . . . . 8  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( X (rem1p `  R ) ( G `  I ) )  e.  I )
6128, 60sseldd 3351 . . . . . . 7  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( X (rem1p `  R ) ( G `  I ) )  e.  ( Base `  P ) )
62 ffvelrn 5871 . . . . . . 7  |-  ( ( ( deg1  `  R ) : ( Base `  P
) --> RR*  /\  ( X (rem1p `  R ) ( G `  I ) )  e.  ( Base `  P ) )  -> 
( ( deg1  `  R ) `  ( X (rem1p `  R
) ( G `  I ) ) )  e.  RR* )
6345, 61, 62sylancr 646 . . . . . 6  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( deg1  `
 R ) `  ( X (rem1p `  R ) ( G `  I ) ) )  e.  RR* )
6428ssdifd 3485 . . . . . . . . . 10  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
I  \  { ( 0g `  P ) } )  C_  ( ( Base `  P )  \  { ( 0g `  P ) } ) )
65 imass2 5243 . . . . . . . . . 10  |-  ( ( I  \  { ( 0g `  P ) } )  C_  (
( Base `  P )  \  { ( 0g `  P ) } )  ->  ( ( deg1  `  R
) " ( I 
\  { ( 0g
`  P ) } ) )  C_  (
( deg1  `
 R ) "
( ( Base `  P
)  \  { ( 0g `  P ) } ) ) )
6664, 65syl 16 . . . . . . . . 9  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( deg1  `
 R ) "
( I  \  {
( 0g `  P
) } ) ) 
C_  ( ( deg1  `  R
) " ( (
Base `  P )  \  { ( 0g `  P ) } ) ) )
6732, 2, 15, 6deg1n0ima 20017 . . . . . . . . . . 11  |-  ( R  e.  Ring  ->  ( ( deg1  `  R ) " (
( Base `  P )  \  { ( 0g `  P ) } ) )  C_  NN0 )
6826, 67syl 16 . . . . . . . . . 10  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( deg1  `
 R ) "
( ( Base `  P
)  \  { ( 0g `  P ) } ) )  C_  NN0 )
69 nn0uz 10525 . . . . . . . . . 10  |-  NN0  =  ( ZZ>= `  0 )
7068, 69syl6sseq 3396 . . . . . . . . 9  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( deg1  `
 R ) "
( ( Base `  P
)  \  { ( 0g `  P ) } ) )  C_  ( ZZ>=
`  0 ) )
7166, 70sstrd 3360 . . . . . . . 8  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( deg1  `
 R ) "
( I  \  {
( 0g `  P
) } ) ) 
C_  ( ZZ>= `  0
) )
72 uzssz 10510 . . . . . . . . 9  |-  ( ZZ>= ` 
0 )  C_  ZZ
73 zssre 10294 . . . . . . . . . 10  |-  ZZ  C_  RR
74 ressxr 9134 . . . . . . . . . 10  |-  RR  C_  RR*
7573, 74sstri 3359 . . . . . . . . 9  |-  ZZ  C_  RR*
7672, 75sstri 3359 . . . . . . . 8  |-  ( ZZ>= ` 
0 )  C_  RR*
7771, 76syl6ss 3362 . . . . . . 7  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( deg1  `
 R ) "
( I  \  {
( 0g `  P
) } ) ) 
C_  RR* )
787, 15lidl0cl 16288 . . . . . . . . . . . 12  |-  ( ( P  e.  Ring  /\  I  e.  U )  ->  ( 0g `  P )  e.  I )
7953, 27, 78syl2anc 644 . . . . . . . . . . 11  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( 0g `  P )  e.  I )
8079snssd 3945 . . . . . . . . . 10  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  { ( 0g `  P ) }  C_  I )
8131necomd 2689 . . . . . . . . . 10  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  { ( 0g `  P ) }  =/=  I )
82 pssdifn0 3691 . . . . . . . . . 10  |-  ( ( { ( 0g `  P ) }  C_  I  /\  { ( 0g
`  P ) }  =/=  I )  -> 
( I  \  {
( 0g `  P
) } )  =/=  (/) )
8380, 81, 82syl2anc 644 . . . . . . . . 9  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
I  \  { ( 0g `  P ) } )  =/=  (/) )
84 ffn 5594 . . . . . . . . . . . 12  |-  ( ( deg1  `  R ) : (
Base `  P ) --> RR* 
->  ( deg1  `  R )  Fn  ( Base `  P
) )
8545, 84ax-mp 5 . . . . . . . . . . 11  |-  ( deg1  `  R
)  Fn  ( Base `  P )
8628ssdifssd 3487 . . . . . . . . . . 11  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
I  \  { ( 0g `  P ) } )  C_  ( Base `  P ) )
87 fnimaeq0 5569 . . . . . . . . . . 11  |-  ( ( ( deg1  `  R )  Fn  ( Base `  P
)  /\  ( I  \  { ( 0g `  P ) } ) 
C_  ( Base `  P
) )  ->  (
( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) )  =  (/)  <->  ( I  \  { ( 0g `  P ) } )  =  (/) ) )
8885, 86, 87sylancr 646 . . . . . . . . . 10  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) )  =  (/)  <->  ( I  \  { ( 0g `  P ) } )  =  (/) ) )
8988necon3bid 2638 . . . . . . . . 9  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) )  =/=  (/)  <->  ( I  \  { ( 0g `  P ) } )  =/=  (/) ) )
9083, 89mpbird 225 . . . . . . . 8  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( deg1  `
 R ) "
( I  \  {
( 0g `  P
) } ) )  =/=  (/) )
91 infmssuzcl 10564 . . . . . . . 8  |-  ( ( ( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) )  C_  ( ZZ>= ` 
0 )  /\  (
( deg1  `
 R ) "
( I  \  {
( 0g `  P
) } ) )  =/=  (/) )  ->  sup ( ( ( deg1  `  R
) " ( I 
\  { ( 0g
`  P ) } ) ) ,  RR ,  `'  <  )  e.  ( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) ) )
9271, 90, 91syl2anc 644 . . . . . . 7  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  sup ( ( ( deg1  `  R
) " ( I 
\  { ( 0g
`  P ) } ) ) ,  RR ,  `'  <  )  e.  ( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) ) )
9377, 92sseldd 3351 . . . . . 6  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  sup ( ( ( deg1  `  R
) " ( I 
\  { ( 0g
`  P ) } ) ) ,  RR ,  `'  <  )  e. 
RR* )
94 xrltnle 9149 . . . . . 6  |-  ( ( ( ( deg1  `  R ) `  ( X (rem1p `  R
) ( G `  I ) ) )  e.  RR*  /\  sup (
( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) ) ,  RR ,  `'  <  )  e.  RR* )  ->  ( ( ( deg1  `  R ) `  ( X (rem1p `  R ) ( G `  I ) ) )  <  sup ( ( ( deg1  `  R
) " ( I 
\  { ( 0g
`  P ) } ) ) ,  RR ,  `'  <  )  <->  -.  sup (
( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) ) ,  RR ,  `'  <  )  <_  (
( deg1  `
 R ) `  ( X (rem1p `  R ) ( G `  I ) ) ) ) )
9563, 93, 94syl2anc 644 . . . . 5  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( ( deg1  `  R ) `  ( X (rem1p `  R
) ( G `  I ) ) )  <  sup ( ( ( deg1  `  R ) " (
I  \  { ( 0g `  P ) } ) ) ,  RR ,  `'  <  )  <->  -.  sup (
( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) ) ,  RR ,  `'  <  )  <_  (
( deg1  `
 R ) `  ( X (rem1p `  R ) ( G `  I ) ) ) ) )
9644, 95mpbid 203 . . . 4  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  -.  sup ( ( ( deg1  `  R
) " ( I 
\  { ( 0g
`  P ) } ) ) ,  RR ,  `'  <  )  <_ 
( ( deg1  `  R ) `  ( X (rem1p `  R
) ( G `  I ) ) ) )
9771adantr 453 . . . . . . 7  |-  ( ( ( ( R  e.  DivRing 
/\  I  e.  U  /\  X  e.  I
)  /\  I  =/=  { ( 0g `  P
) } )  /\  ( X (rem1p `  R ) ( G `  I ) )  =/=  ( 0g
`  P ) )  ->  ( ( deg1  `  R
) " ( I 
\  { ( 0g
`  P ) } ) )  C_  ( ZZ>=
`  0 ) )
9885a1i 11 . . . . . . . 8  |-  ( ( ( ( R  e.  DivRing 
/\  I  e.  U  /\  X  e.  I
)  /\  I  =/=  { ( 0g `  P
) } )  /\  ( X (rem1p `  R ) ( G `  I ) )  =/=  ( 0g
`  P ) )  ->  ( deg1  `  R )  Fn  ( Base `  P
) )
9986adantr 453 . . . . . . . 8  |-  ( ( ( ( R  e.  DivRing 
/\  I  e.  U  /\  X  e.  I
)  /\  I  =/=  { ( 0g `  P
) } )  /\  ( X (rem1p `  R ) ( G `  I ) )  =/=  ( 0g
`  P ) )  ->  ( I  \  { ( 0g `  P ) } ) 
C_  ( Base `  P
) )
10060adantr 453 . . . . . . . . 9  |-  ( ( ( ( R  e.  DivRing 
/\  I  e.  U  /\  X  e.  I
)  /\  I  =/=  { ( 0g `  P
) } )  /\  ( X (rem1p `  R ) ( G `  I ) )  =/=  ( 0g
`  P ) )  ->  ( X (rem1p `  R ) ( G `
 I ) )  e.  I )
101 simpr 449 . . . . . . . . 9  |-  ( ( ( ( R  e.  DivRing 
/\  I  e.  U  /\  X  e.  I
)  /\  I  =/=  { ( 0g `  P
) } )  /\  ( X (rem1p `  R ) ( G `  I ) )  =/=  ( 0g
`  P ) )  ->  ( X (rem1p `  R ) ( G `
 I ) )  =/=  ( 0g `  P ) )
102 eldifsn 3929 . . . . . . . . 9  |-  ( ( X (rem1p `  R ) ( G `  I ) )  e.  ( I 
\  { ( 0g
`  P ) } )  <->  ( ( X (rem1p `  R ) ( G `  I ) )  e.  I  /\  ( X (rem1p `  R ) ( G `  I ) )  =/=  ( 0g
`  P ) ) )
103100, 101, 102sylanbrc 647 . . . . . . . 8  |-  ( ( ( ( R  e.  DivRing 
/\  I  e.  U  /\  X  e.  I
)  /\  I  =/=  { ( 0g `  P
) } )  /\  ( X (rem1p `  R ) ( G `  I ) )  =/=  ( 0g
`  P ) )  ->  ( X (rem1p `  R ) ( G `
 I ) )  e.  ( I  \  { ( 0g `  P ) } ) )
104 fnfvima 5979 . . . . . . . 8  |-  ( ( ( deg1  `  R )  Fn  ( Base `  P
)  /\  ( I  \  { ( 0g `  P ) } ) 
C_  ( Base `  P
)  /\  ( X
(rem1p `
 R ) ( G `  I ) )  e.  ( I 
\  { ( 0g
`  P ) } ) )  ->  (
( deg1  `
 R ) `  ( X (rem1p `  R ) ( G `  I ) ) )  e.  ( ( deg1  `  R ) "
( I  \  {
( 0g `  P
) } ) ) )
10598, 99, 103, 104syl3anc 1185 . . . . . . 7  |-  ( ( ( ( R  e.  DivRing 
/\  I  e.  U  /\  X  e.  I
)  /\  I  =/=  { ( 0g `  P
) } )  /\  ( X (rem1p `  R ) ( G `  I ) )  =/=  ( 0g
`  P ) )  ->  ( ( deg1  `  R
) `  ( X
(rem1p `
 R ) ( G `  I ) ) )  e.  ( ( deg1  `  R ) "
( I  \  {
( 0g `  P
) } ) ) )
106 infmssuzle 10563 . . . . . . 7  |-  ( ( ( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) )  C_  ( ZZ>= ` 
0 )  /\  (
( deg1  `
 R ) `  ( X (rem1p `  R ) ( G `  I ) ) )  e.  ( ( deg1  `  R ) "
( I  \  {
( 0g `  P
) } ) ) )  ->  sup (
( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) ) ,  RR ,  `'  <  )  <_  (
( deg1  `
 R ) `  ( X (rem1p `  R ) ( G `  I ) ) ) )
10797, 105, 106syl2anc 644 . . . . . 6  |-  ( ( ( ( R  e.  DivRing 
/\  I  e.  U  /\  X  e.  I
)  /\  I  =/=  { ( 0g `  P
) } )  /\  ( X (rem1p `  R ) ( G `  I ) )  =/=  ( 0g
`  P ) )  ->  sup ( ( ( deg1  `  R ) " (
I  \  { ( 0g `  P ) } ) ) ,  RR ,  `'  <  )  <_ 
( ( deg1  `  R ) `  ( X (rem1p `  R
) ( G `  I ) ) ) )
108107ex 425 . . . . 5  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( X (rem1p `  R
) ( G `  I ) )  =/=  ( 0g `  P
)  ->  sup (
( ( deg1  `  R ) " ( I  \  { ( 0g `  P ) } ) ) ,  RR ,  `'  <  )  <_  (
( deg1  `
 R ) `  ( X (rem1p `  R ) ( G `  I ) ) ) ) )
109108necon1bd 2674 . . . 4  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( -.  sup ( ( ( deg1  `  R ) " (
I  \  { ( 0g `  P ) } ) ) ,  RR ,  `'  <  )  <_ 
( ( deg1  `  R ) `  ( X (rem1p `  R
) ( G `  I ) ) )  ->  ( X (rem1p `  R ) ( G `
 I ) )  =  ( 0g `  P ) ) )
11096, 109mpd 15 . . 3  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( X (rem1p `  R ) ( G `  I ) )  =  ( 0g
`  P ) )
1112, 14, 6, 37, 15, 40dvdsr1p 20089 . . . 4  |-  ( ( R  e.  Ring  /\  X  e.  ( Base `  P
)  /\  ( G `  I )  e.  (Unic1p `  R ) )  -> 
( ( G `  I )  .||  X  <->  ( X
(rem1p `
 R ) ( G `  I ) )  =  ( 0g
`  P ) ) )
11226, 30, 39, 111syl3anc 1185 . . 3  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  (
( G `  I
)  .||  X  <->  ( X
(rem1p `
 R ) ( G `  I ) )  =  ( 0g
`  P ) ) )
113110, 112mpbird 225 . 2  |-  ( ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  /\  I  =/=  { ( 0g `  P ) } )  ->  ( G `  I )  .|| 
X )
11424, 113pm2.61dane 2684 1  |-  ( ( R  e.  DivRing  /\  I  e.  U  /\  X  e.  I )  ->  ( G `  I )  .|| 
X )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360    /\ w3a 937    = wceq 1653    e. wcel 1726    =/= wne 2601    \ cdif 3319    C_ wss 3322   (/)c0 3630   {csn 3816   class class class wbr 4215   `'ccnv 4880   "cima 4884    Fn wfn 5452   -->wf 5453   ` cfv 5457  (class class class)co 6084   supcsup 7448   RRcr 8994   0cc0 8995   RR*cxr 9124    < clt 9125    <_ cle 9126   NN0cn0 10226   ZZcz 10287   ZZ>=cuz 10493   Basecbs 13474   .rcmulr 13535   0gc0g 13728   -gcsg 14693   Ringcrg 15665   ||rcdsr 15748   DivRingcdr 15840  LIdealclidl 16247  Poly1cpl1 16576   deg1 cdg1 19982  Monic1pcmn1 20053  Unic1pcuc1p 20054  quot1pcq1p 20055  rem1pcr1p 20056  idlGen1pcig1p 20057
This theorem is referenced by:  ig1prsp  20105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-inf2 7599  ax-cnex 9051  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072  ax-pre-sup 9073  ax-addf 9074  ax-mulf 9075
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-iin 4098  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-se 4545  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-isom 5466  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-of 6308  df-ofr 6309  df-1st 6352  df-2nd 6353  df-tpos 6482  df-riota 6552  df-recs 6636  df-rdg 6671  df-1o 6727  df-2o 6728  df-oadd 6731  df-er 6908  df-map 7023  df-pm 7024  df-ixp 7067  df-en 7113  df-dom 7114  df-sdom 7115  df-fin 7116  df-sup 7449  df-oi 7482  df-card 7831  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-nn 10006  df-2 10063  df-3 10064  df-4 10065  df-5 10066  df-6 10067  df-7 10068  df-8 10069  df-9 10070  df-10 10071  df-n0 10227  df-z 10288  df-dec 10388  df-uz 10494  df-fz 11049  df-fzo 11141  df-seq 11329  df-hash 11624  df-struct 13476  df-ndx 13477  df-slot 13478  df-base 13479  df-sets 13480  df-ress 13481  df-plusg 13547  df-mulr 13548  df-starv 13549  df-sca 13550  df-vsca 13551  df-tset 13553  df-ple 13554  df-ds 13556  df-unif 13557  df-0g 13732  df-gsum 13733  df-mre 13816  df-mrc 13817  df-acs 13819  df-mnd 14695  df-mhm 14743  df-submnd 14744  df-grp 14817  df-minusg 14818  df-sbg 14819  df-mulg 14820  df-subg 14946  df-ghm 15009  df-cntz 15121  df-cmn 15419  df-abl 15420  df-mgp 15654  df-rng 15668  df-cring 15669  df-ur 15670  df-oppr 15733  df-dvdsr 15751  df-unit 15752  df-invr 15782  df-drng 15842  df-subrg 15871  df-lmod 15957  df-lss 16014  df-sra 16249  df-rgmod 16250  df-lidl 16251  df-rlreg 16348  df-ascl 16379  df-psr 16422  df-mvr 16423  df-mpl 16424  df-opsr 16430  df-psr1 16581  df-vr1 16582  df-ply1 16583  df-coe1 16586  df-cnfld 16709  df-mdeg 19983  df-deg1 19984  df-mon1 20058  df-uc1p 20059  df-q1p 20060  df-r1p 20061  df-ig1p 20062
  Copyright terms: Public domain W3C validator