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

Theorem fta1g 21642
Description: The one-sided fundamental theorem of algebra. A polynomial of degree  n has at most  n roots. Unlike the real fundamental theorem fta 22420, which is only true in  CC and other algebraically closed fields, this is true in any integral domain. (Contributed by Mario Carneiro, 12-Jun-2015.)
Hypotheses
Ref Expression
fta1g.p  |-  P  =  (Poly1 `  R )
fta1g.b  |-  B  =  ( Base `  P
)
fta1g.d  |-  D  =  ( deg1  `  R )
fta1g.o  |-  O  =  (eval1 `  R )
fta1g.w  |-  W  =  ( 0g `  R
)
fta1g.z  |-  .0.  =  ( 0g `  P )
fta1g.1  |-  ( ph  ->  R  e. IDomn )
fta1g.2  |-  ( ph  ->  F  e.  B )
fta1g.3  |-  ( ph  ->  F  =/=  .0.  )
Assertion
Ref Expression
fta1g  |-  ( ph  ->  ( # `  ( `' ( O `  F ) " { W } ) )  <_ 
( D `  F
) )

Proof of Theorem fta1g
Dummy variables  f 
d  g  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2443 . 2  |-  ( D `
 F )  =  ( D `  F
)
2 fta1g.2 . . 3  |-  ( ph  ->  F  e.  B )
3 fta1g.1 . . . . . 6  |-  ( ph  ->  R  e. IDomn )
4 isidom 17379 . . . . . . 7  |-  ( R  e. IDomn 
<->  ( R  e.  CRing  /\  R  e. Domn ) )
54simplbi 460 . . . . . 6  |-  ( R  e. IDomn  ->  R  e.  CRing )
6 crngrng 16658 . . . . . 6  |-  ( R  e.  CRing  ->  R  e.  Ring )
73, 5, 63syl 20 . . . . 5  |-  ( ph  ->  R  e.  Ring )
8 fta1g.3 . . . . 5  |-  ( ph  ->  F  =/=  .0.  )
9 fta1g.d . . . . . 6  |-  D  =  ( deg1  `  R )
10 fta1g.p . . . . . 6  |-  P  =  (Poly1 `  R )
11 fta1g.z . . . . . 6  |-  .0.  =  ( 0g `  P )
12 fta1g.b . . . . . 6  |-  B  =  ( Base `  P
)
139, 10, 11, 12deg1nn0cl 21562 . . . . 5  |-  ( ( R  e.  Ring  /\  F  e.  B  /\  F  =/= 
.0.  )  ->  ( D `  F )  e.  NN0 )
147, 2, 8, 13syl3anc 1218 . . . 4  |-  ( ph  ->  ( D `  F
)  e.  NN0 )
15 eqeq2 2452 . . . . . . . 8  |-  ( x  =  0  ->  (
( D `  f
)  =  x  <->  ( D `  f )  =  0 ) )
1615imbi1d 317 . . . . . . 7  |-  ( x  =  0  ->  (
( ( D `  f )  =  x  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  <->  ( ( D `  f )  =  0  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
1716ralbidv 2738 . . . . . 6  |-  ( x  =  0  ->  ( A. f  e.  B  ( ( D `  f )  =  x  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  <->  A. f  e.  B  ( ( D `  f )  =  0  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
1817imbi2d 316 . . . . 5  |-  ( x  =  0  ->  (
( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f
)  =  x  -> 
( # `  ( `' ( O `  f
) " { W } ) )  <_ 
( D `  f
) ) )  <->  ( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f )  =  0  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) ) ) ) )
19 eqeq2 2452 . . . . . . . 8  |-  ( x  =  d  ->  (
( D `  f
)  =  x  <->  ( D `  f )  =  d ) )
2019imbi1d 317 . . . . . . 7  |-  ( x  =  d  ->  (
( ( D `  f )  =  x  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  <->  ( ( D `  f )  =  d  ->  ( # `  ( `' ( O `
 f ) " { W } ) )  <_  ( D `  f ) ) ) )
2120ralbidv 2738 . . . . . 6  |-  ( x  =  d  ->  ( A. f  e.  B  ( ( D `  f )  =  x  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  <->  A. f  e.  B  ( ( D `  f )  =  d  ->  ( # `  ( `' ( O `
 f ) " { W } ) )  <_  ( D `  f ) ) ) )
2221imbi2d 316 . . . . 5  |-  ( x  =  d  ->  (
( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f
)  =  x  -> 
( # `  ( `' ( O `  f
) " { W } ) )  <_ 
( D `  f
) ) )  <->  ( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f )  =  d  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) ) ) ) )
23 eqeq2 2452 . . . . . . . 8  |-  ( x  =  ( d  +  1 )  ->  (
( D `  f
)  =  x  <->  ( D `  f )  =  ( d  +  1 ) ) )
2423imbi1d 317 . . . . . . 7  |-  ( x  =  ( d  +  1 )  ->  (
( ( D `  f )  =  x  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  <->  ( ( D `  f )  =  ( d  +  1 )  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
2524ralbidv 2738 . . . . . 6  |-  ( x  =  ( d  +  1 )  ->  ( A. f  e.  B  ( ( D `  f )  =  x  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  <->  A. f  e.  B  ( ( D `  f )  =  ( d  +  1 )  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
2625imbi2d 316 . . . . 5  |-  ( x  =  ( d  +  1 )  ->  (
( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f
)  =  x  -> 
( # `  ( `' ( O `  f
) " { W } ) )  <_ 
( D `  f
) ) )  <->  ( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f )  =  ( d  +  1 )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) ) ) ) )
27 eqeq2 2452 . . . . . . . 8  |-  ( x  =  ( D `  F )  ->  (
( D `  f
)  =  x  <->  ( D `  f )  =  ( D `  F ) ) )
2827imbi1d 317 . . . . . . 7  |-  ( x  =  ( D `  F )  ->  (
( ( D `  f )  =  x  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  <->  ( ( D `  f )  =  ( D `  F )  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
2928ralbidv 2738 . . . . . 6  |-  ( x  =  ( D `  F )  ->  ( A. f  e.  B  ( ( D `  f )  =  x  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  <->  A. f  e.  B  ( ( D `  f )  =  ( D `  F )  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
3029imbi2d 316 . . . . 5  |-  ( x  =  ( D `  F )  ->  (
( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f
)  =  x  -> 
( # `  ( `' ( O `  f
) " { W } ) )  <_ 
( D `  f
) ) )  <->  ( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f )  =  ( D `  F )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) ) ) ) )
31 simprr 756 . . . . . . . . . . . . . 14  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( D `  f )  =  0 )
32 0nn0 10597 . . . . . . . . . . . . . 14  |-  0  e.  NN0
3331, 32syl6eqel 2531 . . . . . . . . . . . . 13  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( D `  f )  e.  NN0 )
345, 6syl 16 . . . . . . . . . . . . . 14  |-  ( R  e. IDomn  ->  R  e.  Ring )
35 simpl 457 . . . . . . . . . . . . . 14  |-  ( ( f  e.  B  /\  ( D `  f )  =  0 )  -> 
f  e.  B )
369, 10, 11, 12deg1nn0clb 21564 . . . . . . . . . . . . . 14  |-  ( ( R  e.  Ring  /\  f  e.  B )  ->  (
f  =/=  .0.  <->  ( D `  f )  e.  NN0 ) )
3734, 35, 36syl2an 477 . . . . . . . . . . . . 13  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( f  =/= 
.0. 
<->  ( D `  f
)  e.  NN0 )
)
3833, 37mpbird 232 . . . . . . . . . . . 12  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  f  =/=  .0.  )
39 simplrr 760 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( D `  f
)  =  0 )
40 0le0 10414 . . . . . . . . . . . . . . . . 17  |-  0  <_  0
4139, 40syl6eqbr 4332 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( D `  f
)  <_  0 )
4234ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  ->  R  e.  Ring )
43 simplrl 759 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
f  e.  B )
44 eqid 2443 . . . . . . . . . . . . . . . . . 18  |-  (algSc `  P )  =  (algSc `  P )
459, 10, 12, 44deg1le0 21586 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  Ring  /\  f  e.  B )  ->  (
( D `  f
)  <_  0  <->  f  =  ( (algSc `  P ) `  ( (coe1 `  f ) ` 
0 ) ) ) )
4642, 43, 45syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( ( D `  f )  <_  0  <->  f  =  ( (algSc `  P ) `  (
(coe1 `  f ) ` 
0 ) ) ) )
4741, 46mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
f  =  ( (algSc `  P ) `  (
(coe1 `  f ) ` 
0 ) ) )
4847fveq2d 5698 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( O `  f
)  =  ( O `
 ( (algSc `  P ) `  (
(coe1 `  f ) ` 
0 ) ) ) )
495adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  R  e.  CRing )
5049adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  ->  R  e.  CRing )
51 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (coe1 `  f
)  =  (coe1 `  f
)
52 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Base `  R )  =  (
Base `  R )
5351, 12, 10, 52coe1f 17670 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  e.  B  ->  (coe1 `  f ) : NN0 --> (
Base `  R )
)
5443, 53syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
(coe1 `  f ) : NN0 --> ( Base `  R
) )
55 ffvelrn 5844 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( (coe1 `  f ) : NN0 --> ( Base `  R
)  /\  0  e.  NN0 )  ->  ( (coe1 `  f ) `  0
)  e.  ( Base `  R ) )
5654, 32, 55sylancl 662 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( (coe1 `  f ) ` 
0 )  e.  (
Base `  R )
)
57 fta1g.o . . . . . . . . . . . . . . . . . . . . 21  |-  O  =  (eval1 `  R )
5857, 10, 52, 44evl1sca 17771 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e.  CRing  /\  (
(coe1 `  f ) ` 
0 )  e.  (
Base `  R )
)  ->  ( O `  ( (algSc `  P
) `  ( (coe1 `  f ) `  0
) ) )  =  ( ( Base `  R
)  X.  { ( (coe1 `  f ) ` 
0 ) } ) )
5950, 56, 58syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( O `  (
(algSc `  P ) `  ( (coe1 `  f ) ` 
0 ) ) )  =  ( ( Base `  R )  X.  {
( (coe1 `  f ) ` 
0 ) } ) )
6048, 59eqtrd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( O `  f
)  =  ( (
Base `  R )  X.  { ( (coe1 `  f
) `  0 ) } ) )
6160fveq1d 5696 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( ( O `  f ) `  x
)  =  ( ( ( Base `  R
)  X.  { ( (coe1 `  f ) ` 
0 ) } ) `
 x ) )
62 eqid 2443 . . . . . . . . . . . . . . . . . . . 20  |-  ( R  ^s  ( Base `  R
) )  =  ( R  ^s  ( Base `  R
) )
63 eqid 2443 . . . . . . . . . . . . . . . . . . . 20  |-  ( Base `  ( R  ^s  ( Base `  R ) ) )  =  ( Base `  ( R  ^s  ( Base `  R
) ) )
64 simpl 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  R  e. IDomn )
65 fvex 5704 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Base `  R )  e.  _V
6665a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( Base `  R
)  e.  _V )
6757, 10, 62, 52evl1rhm 17769 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( R  e.  CRing  ->  O  e.  ( P RingHom  ( R  ^s  ( Base `  R ) ) ) )
6812, 63rhmf 16819 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( O  e.  ( P RingHom  ( R  ^s  ( Base `  R
) ) )  ->  O : B --> ( Base `  ( R  ^s  ( Base `  R ) ) ) )
6949, 67, 683syl 20 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  O : B --> ( Base `  ( R  ^s  ( Base `  R )
) ) )
70 simprl 755 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  f  e.  B
)
7169, 70ffvelrnd 5847 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( O `  f )  e.  (
Base `  ( R  ^s  ( Base `  R )
) ) )
7262, 52, 63, 64, 66, 71pwselbas 14430 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( O `  f ) : (
Base `  R ) --> ( Base `  R )
)
73 ffn 5562 . . . . . . . . . . . . . . . . . . 19  |-  ( ( O `  f ) : ( Base `  R
) --> ( Base `  R
)  ->  ( O `  f )  Fn  ( Base `  R ) )
74 fniniseg 5827 . . . . . . . . . . . . . . . . . . 19  |-  ( ( O `  f )  Fn  ( Base `  R
)  ->  ( x  e.  ( `' ( O `
 f ) " { W } )  <->  ( x  e.  ( Base `  R
)  /\  ( ( O `  f ) `  x )  =  W ) ) )
7572, 73, 743syl 20 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( x  e.  ( `' ( O `
 f ) " { W } )  <->  ( x  e.  ( Base `  R
)  /\  ( ( O `  f ) `  x )  =  W ) ) )
7675simplbda 624 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( ( O `  f ) `  x
)  =  W )
7775simprbda 623 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  ->  x  e.  ( Base `  R ) )
78 fvex 5704 . . . . . . . . . . . . . . . . . . 19  |-  ( (coe1 `  f ) `  0
)  e.  _V
7978fvconst2 5936 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( Base `  R
)  ->  ( (
( Base `  R )  X.  { ( (coe1 `  f
) `  0 ) } ) `  x
)  =  ( (coe1 `  f ) `  0
) )
8077, 79syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( ( ( Base `  R )  X.  {
( (coe1 `  f ) ` 
0 ) } ) `
 x )  =  ( (coe1 `  f ) ` 
0 ) )
8161, 76, 803eqtr3rd 2484 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( (coe1 `  f ) ` 
0 )  =  W )
8281fveq2d 5698 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( (algSc `  P
) `  ( (coe1 `  f ) `  0
) )  =  ( (algSc `  P ) `  W ) )
83 fta1g.w . . . . . . . . . . . . . . . . 17  |-  W  =  ( 0g `  R
)
8410, 44, 83, 11ply1scl0 17745 . . . . . . . . . . . . . . . 16  |-  ( R  e.  Ring  ->  ( (algSc `  P ) `  W
)  =  .0.  )
8542, 84syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
( (algSc `  P
) `  W )  =  .0.  )
8647, 82, 853eqtrd 2479 . . . . . . . . . . . . . 14  |-  ( ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  /\  x  e.  ( `' ( O `  f ) " { W } ) )  -> 
f  =  .0.  )
8786ex 434 . . . . . . . . . . . . 13  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( x  e.  ( `' ( O `
 f ) " { W } )  -> 
f  =  .0.  )
)
8887necon3ad 2647 . . . . . . . . . . . 12  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( f  =/= 
.0.  ->  -.  x  e.  ( `' ( O `  f ) " { W } ) ) )
8938, 88mpd 15 . . . . . . . . . . 11  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  -.  x  e.  ( `' ( O `  f ) " { W } ) )
9089eq0rdv 3675 . . . . . . . . . 10  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( `' ( O `  f )
" { W }
)  =  (/) )
9190fveq2d 5698 . . . . . . . . 9  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  =  ( # `  (/) ) )
92 hash0 12138 . . . . . . . . 9  |-  ( # `  (/) )  =  0
9391, 92syl6eq 2491 . . . . . . . 8  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  =  0 )
9440, 31syl5breqr 4331 . . . . . . . 8  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  0  <_  ( D `  f )
)
9593, 94eqbrtrd 4315 . . . . . . 7  |-  ( ( R  e. IDomn  /\  (
f  e.  B  /\  ( D `  f )  =  0 ) )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )
9695expr 615 . . . . . 6  |-  ( ( R  e. IDomn  /\  f  e.  B )  ->  (
( D `  f
)  =  0  -> 
( # `  ( `' ( O `  f
) " { W } ) )  <_ 
( D `  f
) ) )
9796ralrimiva 2802 . . . . 5  |-  ( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f )  =  0  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) ) )
98 fveq2 5694 . . . . . . . . . . 11  |-  ( f  =  g  ->  ( D `  f )  =  ( D `  g ) )
9998eqeq1d 2451 . . . . . . . . . 10  |-  ( f  =  g  ->  (
( D `  f
)  =  d  <->  ( D `  g )  =  d ) )
100 fveq2 5694 . . . . . . . . . . . . . 14  |-  ( f  =  g  ->  ( O `  f )  =  ( O `  g ) )
101100cnveqd 5018 . . . . . . . . . . . . 13  |-  ( f  =  g  ->  `' ( O `  f )  =  `' ( O `
 g ) )
102101imaeq1d 5171 . . . . . . . . . . . 12  |-  ( f  =  g  ->  ( `' ( O `  f ) " { W } )  =  ( `' ( O `  g ) " { W } ) )
103102fveq2d 5698 . . . . . . . . . . 11  |-  ( f  =  g  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  =  (
# `  ( `' ( O `  g )
" { W }
) ) )
104103, 98breq12d 4308 . . . . . . . . . 10  |-  ( f  =  g  ->  (
( # `  ( `' ( O `  f
) " { W } ) )  <_ 
( D `  f
)  <->  ( # `  ( `' ( O `  g ) " { W } ) )  <_ 
( D `  g
) ) )
10599, 104imbi12d 320 . . . . . . . . 9  |-  ( f  =  g  ->  (
( ( D `  f )  =  d  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  <->  ( ( D `  g )  =  d  ->  ( # `  ( `' ( O `
 g ) " { W } ) )  <_  ( D `  g ) ) ) )
106105cbvralv 2950 . . . . . . . 8  |-  ( A. f  e.  B  (
( D `  f
)  =  d  -> 
( # `  ( `' ( O `  f
) " { W } ) )  <_ 
( D `  f
) )  <->  A. g  e.  B  ( ( D `  g )  =  d  ->  ( # `  ( `' ( O `
 g ) " { W } ) )  <_  ( D `  g ) ) )
107 simprr 756 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  (
f  e.  B  /\  ( D `  f )  =  ( d  +  1 ) ) )  ->  ( D `  f )  =  ( d  +  1 ) )
108 peano2nn0 10623 . . . . . . . . . . . . . . . . 17  |-  ( d  e.  NN0  ->  ( d  +  1 )  e. 
NN0 )
109108ad2antlr 726 . . . . . . . . . . . . . . . 16  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  (
f  e.  B  /\  ( D `  f )  =  ( d  +  1 ) ) )  ->  ( d  +  1 )  e.  NN0 )
110107, 109eqeltrd 2517 . . . . . . . . . . . . . . 15  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  (
f  e.  B  /\  ( D `  f )  =  ( d  +  1 ) ) )  ->  ( D `  f )  e.  NN0 )
111110nn0ge0d 10642 . . . . . . . . . . . . . 14  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  (
f  e.  B  /\  ( D `  f )  =  ( d  +  1 ) ) )  ->  0  <_  ( D `  f )
)
112 fveq2 5694 . . . . . . . . . . . . . . . 16  |-  ( ( `' ( O `  f ) " { W } )  =  (/)  ->  ( # `  ( `' ( O `  f ) " { W } ) )  =  ( # `  (/) ) )
113112, 92syl6eq 2491 . . . . . . . . . . . . . . 15  |-  ( ( `' ( O `  f ) " { W } )  =  (/)  ->  ( # `  ( `' ( O `  f ) " { W } ) )  =  0 )
114113breq1d 4305 . . . . . . . . . . . . . 14  |-  ( ( `' ( O `  f ) " { W } )  =  (/)  ->  ( ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
)  <->  0  <_  ( D `  f )
) )
115111, 114syl5ibrcom 222 . . . . . . . . . . . . 13  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  (
f  e.  B  /\  ( D `  f )  =  ( d  +  1 ) ) )  ->  ( ( `' ( O `  f
) " { W } )  =  (/)  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) ) )
116115a1dd 46 . . . . . . . . . . . 12  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  (
f  e.  B  /\  ( D `  f )  =  ( d  +  1 ) ) )  ->  ( ( `' ( O `  f
) " { W } )  =  (/)  ->  ( A. g  e.  B  ( ( D `
 g )  =  d  ->  ( # `  ( `' ( O `  g ) " { W } ) )  <_ 
( D `  g
) )  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
117 n0 3649 . . . . . . . . . . . . 13  |-  ( ( `' ( O `  f ) " { W } )  =/=  (/)  <->  E. x  x  e.  ( `' ( O `  f )
" { W }
) )
118 simplll 757 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  ( f  e.  B  /\  ( D `
 f )  =  ( d  +  1 ) ) )  /\  ( x  e.  ( `' ( O `  f ) " { W } )  /\  A. g  e.  B  (
( D `  g
)  =  d  -> 
( # `  ( `' ( O `  g
) " { W } ) )  <_ 
( D `  g
) ) ) )  ->  R  e. IDomn )
119 simplrl 759 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  ( f  e.  B  /\  ( D `
 f )  =  ( d  +  1 ) ) )  /\  ( x  e.  ( `' ( O `  f ) " { W } )  /\  A. g  e.  B  (
( D `  g
)  =  d  -> 
( # `  ( `' ( O `  g
) " { W } ) )  <_ 
( D `  g
) ) ) )  ->  f  e.  B
)
120 eqid 2443 . . . . . . . . . . . . . . . 16  |-  (var1 `  R
)  =  (var1 `  R
)
121 eqid 2443 . . . . . . . . . . . . . . . 16  |-  ( -g `  P )  =  (
-g `  P )
122 eqid 2443 . . . . . . . . . . . . . . . 16  |-  ( (var1 `  R ) ( -g `  P ) ( (algSc `  P ) `  x
) )  =  ( (var1 `  R ) (
-g `  P )
( (algSc `  P
) `  x )
)
123 simpllr 758 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  ( f  e.  B  /\  ( D `
 f )  =  ( d  +  1 ) ) )  /\  ( x  e.  ( `' ( O `  f ) " { W } )  /\  A. g  e.  B  (
( D `  g
)  =  d  -> 
( # `  ( `' ( O `  g
) " { W } ) )  <_ 
( D `  g
) ) ) )  ->  d  e.  NN0 )
124 simplrr 760 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  ( f  e.  B  /\  ( D `
 f )  =  ( d  +  1 ) ) )  /\  ( x  e.  ( `' ( O `  f ) " { W } )  /\  A. g  e.  B  (
( D `  g
)  =  d  -> 
( # `  ( `' ( O `  g
) " { W } ) )  <_ 
( D `  g
) ) ) )  ->  ( D `  f )  =  ( d  +  1 ) )
125 simprl 755 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  ( f  e.  B  /\  ( D `
 f )  =  ( d  +  1 ) ) )  /\  ( x  e.  ( `' ( O `  f ) " { W } )  /\  A. g  e.  B  (
( D `  g
)  =  d  -> 
( # `  ( `' ( O `  g
) " { W } ) )  <_ 
( D `  g
) ) ) )  ->  x  e.  ( `' ( O `  f ) " { W } ) )
126 simprr 756 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  ( f  e.  B  /\  ( D `
 f )  =  ( d  +  1 ) ) )  /\  ( x  e.  ( `' ( O `  f ) " { W } )  /\  A. g  e.  B  (
( D `  g
)  =  d  -> 
( # `  ( `' ( O `  g
) " { W } ) )  <_ 
( D `  g
) ) ) )  ->  A. g  e.  B  ( ( D `  g )  =  d  ->  ( # `  ( `' ( O `  g ) " { W } ) )  <_ 
( D `  g
) ) )
12710, 12, 9, 57, 83, 11, 118, 119, 52, 120, 121, 44, 122, 123, 124, 125, 126fta1glem2 21641 . . . . . . . . . . . . . . 15  |-  ( ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  ( f  e.  B  /\  ( D `
 f )  =  ( d  +  1 ) ) )  /\  ( x  e.  ( `' ( O `  f ) " { W } )  /\  A. g  e.  B  (
( D `  g
)  =  d  -> 
( # `  ( `' ( O `  g
) " { W } ) )  <_ 
( D `  g
) ) ) )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )
128127exp32 605 . . . . . . . . . . . . . 14  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  (
f  e.  B  /\  ( D `  f )  =  ( d  +  1 ) ) )  ->  ( x  e.  ( `' ( O `
 f ) " { W } )  -> 
( A. g  e.  B  ( ( D `
 g )  =  d  ->  ( # `  ( `' ( O `  g ) " { W } ) )  <_ 
( D `  g
) )  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
129128exlimdv 1690 . . . . . . . . . . . . 13  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  (
f  e.  B  /\  ( D `  f )  =  ( d  +  1 ) ) )  ->  ( E. x  x  e.  ( `' ( O `  f )
" { W }
)  ->  ( A. g  e.  B  (
( D `  g
)  =  d  -> 
( # `  ( `' ( O `  g
) " { W } ) )  <_ 
( D `  g
) )  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
130117, 129syl5bi 217 . . . . . . . . . . . 12  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  (
f  e.  B  /\  ( D `  f )  =  ( d  +  1 ) ) )  ->  ( ( `' ( O `  f
) " { W } )  =/=  (/)  ->  ( A. g  e.  B  ( ( D `  g )  =  d  ->  ( # `  ( `' ( O `  g ) " { W } ) )  <_ 
( D `  g
) )  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
131116, 130pm2.61dne 2691 . . . . . . . . . . 11  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  (
f  e.  B  /\  ( D `  f )  =  ( d  +  1 ) ) )  ->  ( A. g  e.  B  ( ( D `  g )  =  d  ->  ( # `  ( `' ( O `
 g ) " { W } ) )  <_  ( D `  g ) )  -> 
( # `  ( `' ( O `  f
) " { W } ) )  <_ 
( D `  f
) ) )
132131expr 615 . . . . . . . . . 10  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  f  e.  B )  ->  (
( D `  f
)  =  ( d  +  1 )  -> 
( A. g  e.  B  ( ( D `
 g )  =  d  ->  ( # `  ( `' ( O `  g ) " { W } ) )  <_ 
( D `  g
) )  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
133132com23 78 . . . . . . . . 9  |-  ( ( ( R  e. IDomn  /\  d  e.  NN0 )  /\  f  e.  B )  ->  ( A. g  e.  B  ( ( D `  g )  =  d  ->  ( # `  ( `' ( O `  g ) " { W } ) )  <_ 
( D `  g
) )  ->  (
( D `  f
)  =  ( d  +  1 )  -> 
( # `  ( `' ( O `  f
) " { W } ) )  <_ 
( D `  f
) ) ) )
134133ralrimdva 2809 . . . . . . . 8  |-  ( ( R  e. IDomn  /\  d  e.  NN0 )  ->  ( A. g  e.  B  ( ( D `  g )  =  d  ->  ( # `  ( `' ( O `  g ) " { W } ) )  <_ 
( D `  g
) )  ->  A. f  e.  B  ( ( D `  f )  =  ( d  +  1 )  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
135106, 134syl5bi 217 . . . . . . 7  |-  ( ( R  e. IDomn  /\  d  e.  NN0 )  ->  ( A. f  e.  B  ( ( D `  f )  =  d  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  ->  A. f  e.  B  ( ( D `  f )  =  ( d  +  1 )  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  <_  ( D `  f )
) ) )
136135expcom 435 . . . . . 6  |-  ( d  e.  NN0  ->  ( R  e. IDomn  ->  ( A. f  e.  B  ( ( D `  f )  =  d  ->  ( # `  ( `' ( O `
 f ) " { W } ) )  <_  ( D `  f ) )  ->  A. f  e.  B  ( ( D `  f )  =  ( d  +  1 )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) ) ) ) )
137136a2d 26 . . . . 5  |-  ( d  e.  NN0  ->  ( ( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f )  =  d  ->  ( # `  ( `' ( O `
 f ) " { W } ) )  <_  ( D `  f ) ) )  ->  ( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f )  =  ( d  +  1 )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) ) ) ) )
13818, 22, 26, 30, 97, 137nn0ind 10741 . . . 4  |-  ( ( D `  F )  e.  NN0  ->  ( R  e. IDomn  ->  A. f  e.  B  ( ( D `  f )  =  ( D `  F )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) ) ) )
13914, 3, 138sylc 60 . . 3  |-  ( ph  ->  A. f  e.  B  ( ( D `  f )  =  ( D `  F )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) ) )
140 fveq2 5694 . . . . . 6  |-  ( f  =  F  ->  ( D `  f )  =  ( D `  F ) )
141140eqeq1d 2451 . . . . 5  |-  ( f  =  F  ->  (
( D `  f
)  =  ( D `
 F )  <->  ( D `  F )  =  ( D `  F ) ) )
142 fveq2 5694 . . . . . . . . 9  |-  ( f  =  F  ->  ( O `  f )  =  ( O `  F ) )
143142cnveqd 5018 . . . . . . . 8  |-  ( f  =  F  ->  `' ( O `  f )  =  `' ( O `
 F ) )
144143imaeq1d 5171 . . . . . . 7  |-  ( f  =  F  ->  ( `' ( O `  f ) " { W } )  =  ( `' ( O `  F ) " { W } ) )
145144fveq2d 5698 . . . . . 6  |-  ( f  =  F  ->  ( # `
 ( `' ( O `  f )
" { W }
) )  =  (
# `  ( `' ( O `  F )
" { W }
) ) )
146145, 140breq12d 4308 . . . . 5  |-  ( f  =  F  ->  (
( # `  ( `' ( O `  f
) " { W } ) )  <_ 
( D `  f
)  <->  ( # `  ( `' ( O `  F ) " { W } ) )  <_ 
( D `  F
) ) )
147141, 146imbi12d 320 . . . 4  |-  ( f  =  F  ->  (
( ( D `  f )  =  ( D `  F )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  <->  ( ( D `  F )  =  ( D `  F )  ->  ( # `
 ( `' ( O `  F )
" { W }
) )  <_  ( D `  F )
) ) )
148147rspcv 3072 . . 3  |-  ( F  e.  B  ->  ( A. f  e.  B  ( ( D `  f )  =  ( D `  F )  ->  ( # `  ( `' ( O `  f ) " { W } ) )  <_ 
( D `  f
) )  ->  (
( D `  F
)  =  ( D `
 F )  -> 
( # `  ( `' ( O `  F
) " { W } ) )  <_ 
( D `  F
) ) ) )
1492, 139, 148sylc 60 . 2  |-  ( ph  ->  ( ( D `  F )  =  ( D `  F )  ->  ( # `  ( `' ( O `  F ) " { W } ) )  <_ 
( D `  F
) ) )
1501, 149mpi 17 1  |-  ( ph  ->  ( # `  ( `' ( O `  F ) " { W } ) )  <_ 
( D `  F
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756    =/= wne 2609   A.wral 2718   _Vcvv 2975   (/)c0 3640   {csn 3880   class class class wbr 4295    X. cxp 4841   `'ccnv 4842   "cima 4846    Fn wfn 5416   -->wf 5417   ` cfv 5421  (class class class)co 6094   0cc0 9285   1c1 9286    + caddc 9288    <_ cle 9422   NN0cn0 10582   #chash 12106   Basecbs 14177   0gc0g 14381    ^s cpws 14388   -gcsg 15416   Ringcrg 16648   CRingccrg 16649   RingHom crh 16807  Domncdomn 17354  IDomncidom 17355  algSccascl 17386  var1cv1 17635  Poly1cpl1 17636  coe1cco1 17637  eval1ce1 17752   deg1 cdg1 21526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4406  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-inf2 7850  ax-cnex 9341  ax-resscn 9342  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-mulcom 9349  ax-addass 9350  ax-mulass 9351  ax-distr 9352  ax-i2m1 9353  ax-1ne0 9354  ax-1rid 9355  ax-rnegex 9356  ax-rrecex 9357  ax-cnre 9358  ax-pre-lttri 9359  ax-pre-lttrn 9360  ax-pre-ltadd 9361  ax-pre-mulgt0 9362  ax-pre-sup 9363  ax-addf 9364  ax-mulf 9365
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-nel 2612  df-ral 2723  df-rex 2724  df-reu 2725  df-rmo 2726  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-pss 3347  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-tp 3885  df-op 3887  df-uni 4095  df-int 4132  df-iun 4176  df-iin 4177  df-br 4296  df-opab 4354  df-mpt 4355  df-tr 4389  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-se 4683  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-riota 6055  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-of 6323  df-ofr 6324  df-om 6480  df-1st 6580  df-2nd 6581  df-supp 6694  df-tpos 6748  df-recs 6835  df-rdg 6869  df-1o 6923  df-2o 6924  df-oadd 6927  df-er 7104  df-map 7219  df-pm 7220  df-ixp 7267  df-en 7314  df-dom 7315  df-sdom 7316  df-fin 7317  df-fsupp 7624  df-sup 7694  df-oi 7727  df-card 8112  df-cda 8340  df-pnf 9423  df-mnf 9424  df-xr 9425  df-ltxr 9426  df-le 9427  df-sub 9600  df-neg 9601  df-nn 10326  df-2 10383  df-3 10384  df-4 10385  df-5 10386  df-6 10387  df-7 10388  df-8 10389  df-9 10390  df-10 10391  df-n0 10583  df-z 10650  df-dec 10759  df-uz 10865  df-fz 11441  df-fzo 11552  df-seq 11810  df-hash 12107  df-struct 14179  df-ndx 14180  df-slot 14181  df-base 14182  df-sets 14183  df-ress 14184  df-plusg 14254  df-mulr 14255  df-starv 14256  df-sca 14257  df-vsca 14258  df-ip 14259  df-tset 14260  df-ple 14261  df-ds 14263  df-unif 14264  df-hom 14265  df-cco 14266  df-0g 14383  df-gsum 14384  df-prds 14389  df-pws 14391  df-mre 14527  df-mrc 14528  df-acs 14530  df-mnd 15418  df-mhm 15467  df-submnd 15468  df-grp 15548  df-minusg 15549  df-sbg 15550  df-mulg 15551  df-subg 15681  df-ghm 15748  df-cntz 15838  df-cmn 16282  df-abl 16283  df-mgp 16595  df-ur 16607  df-srg 16611  df-rng 16650  df-cring 16651  df-oppr 16718  df-dvdsr 16736  df-unit 16737  df-invr 16767  df-rnghom 16809  df-subrg 16866  df-lmod 16953  df-lss 17017  df-lsp 17056  df-nzr 17343  df-rlreg 17357  df-domn 17358  df-idom 17359  df-assa 17387  df-asp 17388  df-ascl 17389  df-psr 17426  df-mvr 17427  df-mpl 17428  df-opsr 17430  df-evls 17591  df-evl 17592  df-psr1 17639  df-vr1 17640  df-ply1 17641  df-coe1 17642  df-evl1 17754  df-cnfld 17822  df-mdeg 21527  df-deg1 21528  df-mon1 21605  df-uc1p 21606  df-q1p 21607  df-r1p 21608
This theorem is referenced by:  fta1b  21644  lgsqrlem4  22686  idomrootle  29563
  Copyright terms: Public domain W3C validator