Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  deg1mhm Unicode version

Theorem deg1mhm 27394
Description: Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.)
Hypotheses
Ref Expression
deg1mhm.d  |-  D  =  ( deg1  `  R )
deg1mhm.b  |-  B  =  ( Base `  P
)
deg1mhm.p  |-  P  =  (Poly1 `  R )
deg1mhm.z  |-  .0.  =  ( 0g `  P )
deg1mhm.y  |-  Y  =  ( (mulGrp `  P
)s  ( B  \  {  .0.  } ) )
deg1mhm.n  |-  N  =  (flds  NN0 )
Assertion
Ref Expression
deg1mhm  |-  ( R  e. Domn  ->  ( D  |`  ( B  \  {  .0.  } ) )  e.  ( Y MndHom  N ) )

Proof of Theorem deg1mhm
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 deg1mhm.p . . . . . 6  |-  P  =  (Poly1 `  R )
21ply1domn 19999 . . . . 5  |-  ( R  e. Domn  ->  P  e. Domn )
3 deg1mhm.b . . . . . . 7  |-  B  =  ( Base `  P
)
4 deg1mhm.z . . . . . . 7  |-  .0.  =  ( 0g `  P )
5 eqid 2404 . . . . . . 7  |-  (mulGrp `  P )  =  (mulGrp `  P )
63, 4, 5isdomn3 27391 . . . . . 6  |-  ( P  e. Domn 
<->  ( P  e.  Ring  /\  ( B  \  {  .0.  } )  e.  (SubMnd `  (mulGrp `  P )
) ) )
76simprbi 451 . . . . 5  |-  ( P  e. Domn  ->  ( B  \  {  .0.  } )  e.  (SubMnd `  (mulGrp `  P
) ) )
82, 7syl 16 . . . 4  |-  ( R  e. Domn  ->  ( B  \  {  .0.  } )  e.  (SubMnd `  (mulGrp `  P
) ) )
9 deg1mhm.y . . . . 5  |-  Y  =  ( (mulGrp `  P
)s  ( B  \  {  .0.  } ) )
109submmnd 14709 . . . 4  |-  ( ( B  \  {  .0.  } )  e.  (SubMnd `  (mulGrp `  P ) )  ->  Y  e.  Mnd )
118, 10syl 16 . . 3  |-  ( R  e. Domn  ->  Y  e.  Mnd )
12 nn0subm 16709 . . . 4  |-  NN0  e.  (SubMnd ` fld )
13 deg1mhm.n . . . . 5  |-  N  =  (flds  NN0 )
1413submmnd 14709 . . . 4  |-  ( NN0 
e.  (SubMnd ` fld )  ->  N  e. 
Mnd )
1512, 14mp1i 12 . . 3  |-  ( R  e. Domn  ->  N  e.  Mnd )
1611, 15jca 519 . 2  |-  ( R  e. Domn  ->  ( Y  e. 
Mnd  /\  N  e.  Mnd ) )
17 deg1mhm.d . . . . . . . 8  |-  D  =  ( deg1  `  R )
1817, 1, 3deg1xrf 19957 . . . . . . 7  |-  D : B
--> RR*
19 ffn 5550 . . . . . . 7  |-  ( D : B --> RR*  ->  D  Fn  B )
2018, 19ax-mp 8 . . . . . 6  |-  D  Fn  B
21 difss 3434 . . . . . 6  |-  ( B 
\  {  .0.  }
)  C_  B
22 fnssres 5517 . . . . . 6  |-  ( ( D  Fn  B  /\  ( B  \  {  .0.  } )  C_  B )  ->  ( D  |`  ( B  \  {  .0.  }
) )  Fn  ( B  \  {  .0.  }
) )
2320, 21, 22mp2an 654 . . . . 5  |-  ( D  |`  ( B  \  {  .0.  } ) )  Fn  ( B  \  {  .0.  } )
2423a1i 11 . . . 4  |-  ( R  e. Domn  ->  ( D  |`  ( B  \  {  .0.  } ) )  Fn  ( B  \  {  .0.  }
) )
25 fvres 5704 . . . . . . 7  |-  ( x  e.  ( B  \  {  .0.  } )  -> 
( ( D  |`  ( B  \  {  .0.  } ) ) `  x
)  =  ( D `
 x ) )
2625adantl 453 . . . . . 6  |-  ( ( R  e. Domn  /\  x  e.  ( B  \  {  .0.  } ) )  -> 
( ( D  |`  ( B  \  {  .0.  } ) ) `  x
)  =  ( D `
 x ) )
27 domnrng 16311 . . . . . . . 8  |-  ( R  e. Domn  ->  R  e.  Ring )
2827adantr 452 . . . . . . 7  |-  ( ( R  e. Domn  /\  x  e.  ( B  \  {  .0.  } ) )  ->  R  e.  Ring )
29 eldifi 3429 . . . . . . . 8  |-  ( x  e.  ( B  \  {  .0.  } )  ->  x  e.  B )
3029adantl 453 . . . . . . 7  |-  ( ( R  e. Domn  /\  x  e.  ( B  \  {  .0.  } ) )  ->  x  e.  B )
31 eldifsni 3888 . . . . . . . 8  |-  ( x  e.  ( B  \  {  .0.  } )  ->  x  =/=  .0.  )
3231adantl 453 . . . . . . 7  |-  ( ( R  e. Domn  /\  x  e.  ( B  \  {  .0.  } ) )  ->  x  =/=  .0.  )
3317, 1, 4, 3deg1nn0cl 19964 . . . . . . 7  |-  ( ( R  e.  Ring  /\  x  e.  B  /\  x  =/=  .0.  )  ->  ( D `  x )  e.  NN0 )
3428, 30, 32, 33syl3anc 1184 . . . . . 6  |-  ( ( R  e. Domn  /\  x  e.  ( B  \  {  .0.  } ) )  -> 
( D `  x
)  e.  NN0 )
3526, 34eqeltrd 2478 . . . . 5  |-  ( ( R  e. Domn  /\  x  e.  ( B  \  {  .0.  } ) )  -> 
( ( D  |`  ( B  \  {  .0.  } ) ) `  x
)  e.  NN0 )
3635ralrimiva 2749 . . . 4  |-  ( R  e. Domn  ->  A. x  e.  ( B  \  {  .0.  } ) ( ( D  |`  ( B  \  {  .0.  } ) ) `  x )  e.  NN0 )
37 ffnfv 5853 . . . 4  |-  ( ( D  |`  ( B  \  {  .0.  } ) ) : ( B 
\  {  .0.  }
) --> NN0  <->  ( ( D  |`  ( B  \  {  .0.  } ) )  Fn  ( B  \  {  .0.  } )  /\  A. x  e.  ( B  \  {  .0.  } ) ( ( D  |`  ( B  \  {  .0.  } ) ) `  x
)  e.  NN0 )
)
3824, 36, 37sylanbrc 646 . . 3  |-  ( R  e. Domn  ->  ( D  |`  ( B  \  {  .0.  } ) ) : ( B  \  {  .0.  } ) --> NN0 )
39 eqid 2404 . . . . . 6  |-  (RLReg `  R )  =  (RLReg `  R )
40 eqid 2404 . . . . . 6  |-  ( .r
`  P )  =  ( .r `  P
)
4127adantr 452 . . . . . 6  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  ->  R  e.  Ring )
4229ad2antrl 709 . . . . . 6  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  ->  x  e.  B )
4331ad2antrl 709 . . . . . 6  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  ->  x  =/=  .0.  )
44 simpl 444 . . . . . . 7  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  ->  R  e. Domn )
45 eqid 2404 . . . . . . . 8  |-  (coe1 `  x
)  =  (coe1 `  x
)
4617, 1, 4, 3, 39, 45deg1ldgdomn 19970 . . . . . . 7  |-  ( ( R  e. Domn  /\  x  e.  B  /\  x  =/=  .0.  )  ->  (
(coe1 `  x ) `  ( D `  x ) )  e.  (RLReg `  R ) )
4744, 42, 43, 46syl3anc 1184 . . . . . 6  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  -> 
( (coe1 `  x ) `  ( D `  x ) )  e.  (RLReg `  R ) )
48 eldifi 3429 . . . . . . 7  |-  ( y  e.  ( B  \  {  .0.  } )  -> 
y  e.  B )
4948ad2antll 710 . . . . . 6  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  -> 
y  e.  B )
50 eldifsni 3888 . . . . . . 7  |-  ( y  e.  ( B  \  {  .0.  } )  -> 
y  =/=  .0.  )
5150ad2antll 710 . . . . . 6  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  -> 
y  =/=  .0.  )
5217, 1, 39, 3, 40, 4, 41, 42, 43, 47, 49, 51deg1mul2 19990 . . . . 5  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  -> 
( D `  (
x ( .r `  P ) y ) )  =  ( ( D `  x )  +  ( D `  y ) ) )
53 domnrng 16311 . . . . . . . . . 10  |-  ( P  e. Domn  ->  P  e.  Ring )
542, 53syl 16 . . . . . . . . 9  |-  ( R  e. Domn  ->  P  e.  Ring )
5554adantr 452 . . . . . . . 8  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  ->  P  e.  Ring )
563, 40rngcl 15632 . . . . . . . 8  |-  ( ( P  e.  Ring  /\  x  e.  B  /\  y  e.  B )  ->  (
x ( .r `  P ) y )  e.  B )
5755, 42, 49, 56syl3anc 1184 . . . . . . 7  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  -> 
( x ( .r
`  P ) y )  e.  B )
582adantr 452 . . . . . . . 8  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  ->  P  e. Domn )
593, 40, 4domnmuln0 16313 . . . . . . . 8  |-  ( ( P  e. Domn  /\  (
x  e.  B  /\  x  =/=  .0.  )  /\  ( y  e.  B  /\  y  =/=  .0.  ) )  ->  (
x ( .r `  P ) y )  =/=  .0.  )
6058, 42, 43, 49, 51, 59syl122anc 1193 . . . . . . 7  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  -> 
( x ( .r
`  P ) y )  =/=  .0.  )
61 eldifsn 3887 . . . . . . 7  |-  ( ( x ( .r `  P ) y )  e.  ( B  \  {  .0.  } )  <->  ( (
x ( .r `  P ) y )  e.  B  /\  (
x ( .r `  P ) y )  =/=  .0.  ) )
6257, 60, 61sylanbrc 646 . . . . . 6  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  -> 
( x ( .r
`  P ) y )  e.  ( B 
\  {  .0.  }
) )
63 fvres 5704 . . . . . 6  |-  ( ( x ( .r `  P ) y )  e.  ( B  \  {  .0.  } )  -> 
( ( D  |`  ( B  \  {  .0.  } ) ) `  (
x ( .r `  P ) y ) )  =  ( D `
 ( x ( .r `  P ) y ) ) )
6462, 63syl 16 . . . . 5  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  -> 
( ( D  |`  ( B  \  {  .0.  } ) ) `  (
x ( .r `  P ) y ) )  =  ( D `
 ( x ( .r `  P ) y ) ) )
65 fvres 5704 . . . . . . 7  |-  ( y  e.  ( B  \  {  .0.  } )  -> 
( ( D  |`  ( B  \  {  .0.  } ) ) `  y
)  =  ( D `
 y ) )
6625, 65oveqan12d 6059 . . . . . 6  |-  ( ( x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) )  ->  (
( ( D  |`  ( B  \  {  .0.  } ) ) `  x
)  +  ( ( D  |`  ( B  \  {  .0.  } ) ) `  y ) )  =  ( ( D `  x )  +  ( D `  y ) ) )
6766adantl 453 . . . . 5  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  -> 
( ( ( D  |`  ( B  \  {  .0.  } ) ) `  x )  +  ( ( D  |`  ( B  \  {  .0.  }
) ) `  y
) )  =  ( ( D `  x
)  +  ( D `
 y ) ) )
6852, 64, 673eqtr4d 2446 . . . 4  |-  ( ( R  e. Domn  /\  (
x  e.  ( B 
\  {  .0.  }
)  /\  y  e.  ( B  \  {  .0.  } ) ) )  -> 
( ( D  |`  ( B  \  {  .0.  } ) ) `  (
x ( .r `  P ) y ) )  =  ( ( ( D  |`  ( B  \  {  .0.  }
) ) `  x
)  +  ( ( D  |`  ( B  \  {  .0.  } ) ) `  y ) ) )
6968ralrimivva 2758 . . 3  |-  ( R  e. Domn  ->  A. x  e.  ( B  \  {  .0.  } ) A. y  e.  ( B  \  {  .0.  } ) ( ( D  |`  ( B  \  {  .0.  } ) ) `  ( x ( .r `  P
) y ) )  =  ( ( ( D  |`  ( B  \  {  .0.  } ) ) `  x )  +  ( ( D  |`  ( B  \  {  .0.  } ) ) `  y ) ) )
70 eqid 2404 . . . . . . . 8  |-  ( 1r
`  P )  =  ( 1r `  P
)
713, 70rngidcl 15639 . . . . . . 7  |-  ( P  e.  Ring  ->  ( 1r
`  P )  e.  B )
7254, 71syl 16 . . . . . 6  |-  ( R  e. Domn  ->  ( 1r `  P )  e.  B
)
73 domnnzr 16310 . . . . . . 7  |-  ( P  e. Domn  ->  P  e. NzRing )
7470, 4nzrnz 16286 . . . . . . 7  |-  ( P  e. NzRing  ->  ( 1r `  P )  =/=  .0.  )
752, 73, 743syl 19 . . . . . 6  |-  ( R  e. Domn  ->  ( 1r `  P )  =/=  .0.  )
76 eldifsn 3887 . . . . . 6  |-  ( ( 1r `  P )  e.  ( B  \  {  .0.  } )  <->  ( ( 1r `  P )  e.  B  /\  ( 1r
`  P )  =/= 
.0.  ) )
7772, 75, 76sylanbrc 646 . . . . 5  |-  ( R  e. Domn  ->  ( 1r `  P )  e.  ( B  \  {  .0.  } ) )
78 fvres 5704 . . . . 5  |-  ( ( 1r `  P )  e.  ( B  \  {  .0.  } )  -> 
( ( D  |`  ( B  \  {  .0.  } ) ) `  ( 1r `  P ) )  =  ( D `  ( 1r `  P ) ) )
7977, 78syl 16 . . . 4  |-  ( R  e. Domn  ->  ( ( D  |`  ( B  \  {  .0.  } ) ) `  ( 1r `  P ) )  =  ( D `
 ( 1r `  P ) ) )
805, 70rngidval 15621 . . . . . . 7  |-  ( 1r
`  P )  =  ( 0g `  (mulGrp `  P ) )
819, 80subm0 14711 . . . . . 6  |-  ( ( B  \  {  .0.  } )  e.  (SubMnd `  (mulGrp `  P ) )  ->  ( 1r `  P )  =  ( 0g `  Y ) )
828, 81syl 16 . . . . 5  |-  ( R  e. Domn  ->  ( 1r `  P )  =  ( 0g `  Y ) )
8382fveq2d 5691 . . . 4  |-  ( R  e. Domn  ->  ( ( D  |`  ( B  \  {  .0.  } ) ) `  ( 1r `  P ) )  =  ( ( D  |`  ( B  \  {  .0.  } ) ) `  ( 0g
`  Y ) ) )
84 domnnzr 16310 . . . . 5  |-  ( R  e. Domn  ->  R  e. NzRing )
85 eqid 2404 . . . . . . 7  |-  (Monic1p `  R
)  =  (Monic1p `  R
)
861, 70, 85, 17mon1pid 27392 . . . . . 6  |-  ( R  e. NzRing  ->  ( ( 1r
`  P )  e.  (Monic1p `  R )  /\  ( D `  ( 1r
`  P ) )  =  0 ) )
8786simprd 450 . . . . 5  |-  ( R  e. NzRing  ->  ( D `  ( 1r `  P ) )  =  0 )
8884, 87syl 16 . . . 4  |-  ( R  e. Domn  ->  ( D `  ( 1r `  P ) )  =  0 )
8979, 83, 883eqtr3d 2444 . . 3  |-  ( R  e. Domn  ->  ( ( D  |`  ( B  \  {  .0.  } ) ) `  ( 0g `  Y ) )  =  0 )
9038, 69, 893jca 1134 . 2  |-  ( R  e. Domn  ->  ( ( D  |`  ( B  \  {  .0.  } ) ) : ( B  \  {  .0.  } ) --> NN0  /\  A. x  e.  ( B 
\  {  .0.  }
) A. y  e.  ( B  \  {  .0.  } ) ( ( D  |`  ( B  \  {  .0.  } ) ) `  ( x ( .r `  P
) y ) )  =  ( ( ( D  |`  ( B  \  {  .0.  } ) ) `  x )  +  ( ( D  |`  ( B  \  {  .0.  } ) ) `  y ) )  /\  ( ( D  |`  ( B  \  {  .0.  } ) ) `  ( 0g `  Y ) )  =  0 ) )
915, 3mgpbas 15609 . . . . 5  |-  B  =  ( Base `  (mulGrp `  P ) )
929, 91ressbas2 13475 . . . 4  |-  ( ( B  \  {  .0.  } )  C_  B  ->  ( B  \  {  .0.  } )  =  ( Base `  Y ) )
9321, 92ax-mp 8 . . 3  |-  ( B 
\  {  .0.  }
)  =  ( Base `  Y )
94 nn0sscn 10182 . . . 4  |-  NN0  C_  CC
95 cnfldbas 16662 . . . . 5  |-  CC  =  ( Base ` fld )
9613, 95ressbas2 13475 . . . 4  |-  ( NN0  C_  CC  ->  NN0  =  (
Base `  N )
)
9794, 96ax-mp 8 . . 3  |-  NN0  =  ( Base `  N )
98 fvex 5701 . . . . . 6  |-  ( Base `  P )  e.  _V
993, 98eqeltri 2474 . . . . 5  |-  B  e. 
_V
100 difexg 4311 . . . . 5  |-  ( B  e.  _V  ->  ( B  \  {  .0.  }
)  e.  _V )
10199, 100ax-mp 8 . . . 4  |-  ( B 
\  {  .0.  }
)  e.  _V
1025, 40mgpplusg 15607 . . . . 5  |-  ( .r
`  P )  =  ( +g  `  (mulGrp `  P ) )
1039, 102ressplusg 13526 . . . 4  |-  ( ( B  \  {  .0.  } )  e.  _V  ->  ( .r `  P )  =  ( +g  `  Y
) )
104101, 103ax-mp 8 . . 3  |-  ( .r
`  P )  =  ( +g  `  Y
)
105 nn0ex 10183 . . . 4  |-  NN0  e.  _V
106 cnfldadd 16663 . . . . 5  |-  +  =  ( +g  ` fld )
10713, 106ressplusg 13526 . . . 4  |-  ( NN0 
e.  _V  ->  +  =  ( +g  `  N ) )
108105, 107ax-mp 8 . . 3  |-  +  =  ( +g  `  N )
109 eqid 2404 . . 3  |-  ( 0g
`  Y )  =  ( 0g `  Y
)
110 cnfld0 16680 . . . . 5  |-  0  =  ( 0g ` fld )
11113, 110subm0 14711 . . . 4  |-  ( NN0 
e.  (SubMnd ` fld )  ->  0  =  ( 0g `  N
) )
11212, 111ax-mp 8 . . 3  |-  0  =  ( 0g `  N )
11393, 97, 104, 108, 109, 112ismhm 14695 . 2  |-  ( ( D  |`  ( B  \  {  .0.  } ) )  e.  ( Y MndHom  N )  <->  ( ( Y  e.  Mnd  /\  N  e.  Mnd )  /\  (
( D  |`  ( B  \  {  .0.  }
) ) : ( B  \  {  .0.  } ) --> NN0  /\  A. x  e.  ( B  \  {  .0.  } ) A. y  e.  ( B  \  {  .0.  } ) ( ( D  |`  ( B  \  {  .0.  } ) ) `  ( x ( .r `  P
) y ) )  =  ( ( ( D  |`  ( B  \  {  .0.  } ) ) `  x )  +  ( ( D  |`  ( B  \  {  .0.  } ) ) `  y ) )  /\  ( ( D  |`  ( B  \  {  .0.  } ) ) `  ( 0g `  Y ) )  =  0 ) ) )
11416, 90, 113sylanbrc 646 1  |-  ( R  e. Domn  ->  ( D  |`  ( B  \  {  .0.  } ) )  e.  ( Y MndHom  N ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721    =/= wne 2567   A.wral 2666   _Vcvv 2916    \ cdif 3277    C_ wss 3280   {csn 3774    |` cres 4839    Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   CCcc 8944   0cc0 8946    + caddc 8949   RR*cxr 9075   NN0cn0 10177   Basecbs 13424   ↾s cress 13425   +g cplusg 13484   .rcmulr 13485   0gc0g 13678   Mndcmnd 14639   MndHom cmhm 14691  SubMndcsubmnd 14692  mulGrpcmgp 15603   Ringcrg 15615   1rcur 15617  NzRingcnzr 16283  RLRegcrlreg 16294  Domncdomn 16295  Poly1cpl1 16526  coe1cco1 16529  ℂfldccnfld 16658   deg1 cdg1 19930  Monic1pcmn1 20001
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-ofr 6265  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-fz 11000  df-fzo 11091  df-seq 11279  df-hash 11574  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-starv 13499  df-sca 13500  df-vsca 13501  df-tset 13503  df-ple 13504  df-ds 13506  df-unif 13507  df-0g 13682  df-gsum 13683  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-mhm 14693  df-submnd 14694  df-grp 14767  df-minusg 14768  df-sbg 14769  df-mulg 14770  df-subg 14896  df-ghm 14959  df-cntz 15071  df-cmn 15369  df-abl 15370  df-mgp 15604  df-rng 15618  df-cring 15619  df-ur 15620  df-subrg 15821  df-lmod 15907  df-lss 15964  df-nzr 16284  df-rlreg 16298  df-domn 16299  df-ascl 16329  df-psr 16372  df-mvr 16373  df-mpl 16374  df-opsr 16380  df-psr1 16531  df-vr1 16532  df-ply1 16533  df-coe1 16536  df-cnfld 16659  df-mdeg 19931  df-deg1 19932  df-mon1 20006
  Copyright terms: Public domain W3C validator