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

Theorem evls1sca 18917
Description: Univariate polynomial evaluation maps scalars to constant functions. (Contributed by AV, 8-Sep-2019.)
Hypotheses
Ref Expression
evls1sca.q  |-  Q  =  ( S evalSub1  R )
evls1sca.w  |-  W  =  (Poly1 `  U )
evls1sca.u  |-  U  =  ( Ss  R )
evls1sca.b  |-  B  =  ( Base `  S
)
evls1sca.a  |-  A  =  (algSc `  W )
evls1sca.s  |-  ( ph  ->  S  e.  CRing )
evls1sca.r  |-  ( ph  ->  R  e.  (SubRing `  S
) )
evls1sca.x  |-  ( ph  ->  X  e.  R )
Assertion
Ref Expression
evls1sca  |-  ( ph  ->  ( Q `  ( A `  X )
)  =  ( B  X.  { X }
) )

Proof of Theorem evls1sca
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1on 7206 . . . . . . 7  |-  1o  e.  On
21a1i 11 . . . . . 6  |-  ( ph  ->  1o  e.  On )
3 evls1sca.s . . . . . 6  |-  ( ph  ->  S  e.  CRing )
4 evls1sca.r . . . . . 6  |-  ( ph  ->  R  e.  (SubRing `  S
) )
5 eqid 2423 . . . . . . 7  |-  ( ( 1o evalSub  S ) `  R
)  =  ( ( 1o evalSub  S ) `  R
)
6 eqid 2423 . . . . . . 7  |-  ( 1o mPoly  U )  =  ( 1o mPoly  U )
7 evls1sca.u . . . . . . 7  |-  U  =  ( Ss  R )
8 eqid 2423 . . . . . . 7  |-  ( S  ^s  ( B  ^m  1o ) )  =  ( S  ^s  ( B  ^m  1o ) )
9 evls1sca.b . . . . . . 7  |-  B  =  ( Base `  S
)
105, 6, 7, 8, 9evlsrhm 18749 . . . . . 6  |-  ( ( 1o  e.  On  /\  S  e.  CRing  /\  R  e.  (SubRing `  S )
)  ->  ( ( 1o evalSub  S ) `  R
)  e.  ( ( 1o mPoly  U ) RingHom  ( S  ^s  ( B  ^m  1o ) ) ) )
112, 3, 4, 10syl3anc 1265 . . . . 5  |-  ( ph  ->  ( ( 1o evalSub  S ) `
 R )  e.  ( ( 1o mPoly  U
) RingHom  ( S  ^s  ( B  ^m  1o ) ) ) )
12 eqid 2423 . . . . . 6  |-  ( Base `  ( 1o mPoly  U )
)  =  ( Base `  ( 1o mPoly  U )
)
13 eqid 2423 . . . . . 6  |-  ( Base `  ( S  ^s  ( B  ^m  1o ) ) )  =  ( Base `  ( S  ^s  ( B  ^m  1o ) ) )
1412, 13rhmf 17959 . . . . 5  |-  ( ( ( 1o evalSub  S ) `  R )  e.  ( ( 1o mPoly  U ) RingHom  ( S  ^s  ( B  ^m  1o ) ) )  -> 
( ( 1o evalSub  S ) `
 R ) : ( Base `  ( 1o mPoly  U ) ) --> (
Base `  ( S  ^s  ( B  ^m  1o ) ) ) )
1511, 14syl 17 . . . 4  |-  ( ph  ->  ( ( 1o evalSub  S ) `
 R ) : ( Base `  ( 1o mPoly  U ) ) --> (
Base `  ( S  ^s  ( B  ^m  1o ) ) ) )
16 evls1sca.a . . . . . . 7  |-  A  =  (algSc `  W )
17 eqid 2423 . . . . . . 7  |-  (Scalar `  W )  =  (Scalar `  W )
187subrgring 18016 . . . . . . . . 9  |-  ( R  e.  (SubRing `  S
)  ->  U  e.  Ring )
194, 18syl 17 . . . . . . . 8  |-  ( ph  ->  U  e.  Ring )
20 evls1sca.w . . . . . . . . 9  |-  W  =  (Poly1 `  U )
2120ply1ring 18846 . . . . . . . 8  |-  ( U  e.  Ring  ->  W  e. 
Ring )
2219, 21syl 17 . . . . . . 7  |-  ( ph  ->  W  e.  Ring )
2320ply1lmod 18850 . . . . . . . 8  |-  ( U  e.  Ring  ->  W  e. 
LMod )
2419, 23syl 17 . . . . . . 7  |-  ( ph  ->  W  e.  LMod )
25 eqid 2423 . . . . . . 7  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
26 eqid 2423 . . . . . . 7  |-  ( Base `  W )  =  (
Base `  W )
2716, 17, 22, 24, 25, 26asclf 18566 . . . . . 6  |-  ( ph  ->  A : ( Base `  (Scalar `  W )
) --> ( Base `  W
) )
289subrgss 18014 . . . . . . . . . 10  |-  ( R  e.  (SubRing `  S
)  ->  R  C_  B
)
294, 28syl 17 . . . . . . . . 9  |-  ( ph  ->  R  C_  B )
307, 9ressbas2 15185 . . . . . . . . 9  |-  ( R 
C_  B  ->  R  =  ( Base `  U
) )
3129, 30syl 17 . . . . . . . 8  |-  ( ph  ->  R  =  ( Base `  U ) )
3220ply1sca 18851 . . . . . . . . . 10  |-  ( U  e.  Ring  ->  U  =  (Scalar `  W )
)
3319, 32syl 17 . . . . . . . . 9  |-  ( ph  ->  U  =  (Scalar `  W ) )
3433fveq2d 5891 . . . . . . . 8  |-  ( ph  ->  ( Base `  U
)  =  ( Base `  (Scalar `  W )
) )
3531, 34eqtrd 2464 . . . . . . 7  |-  ( ph  ->  R  =  ( Base `  (Scalar `  W )
) )
36 eqid 2423 . . . . . . . . . 10  |-  (PwSer1 `  U
)  =  (PwSer1 `  U
)
3720, 36, 26ply1bas 18793 . . . . . . . . 9  |-  ( Base `  W )  =  (
Base `  ( 1o mPoly  U ) )
3837a1i 11 . . . . . . . 8  |-  ( ph  ->  ( Base `  W
)  =  ( Base `  ( 1o mPoly  U )
) )
3938eqcomd 2431 . . . . . . 7  |-  ( ph  ->  ( Base `  ( 1o mPoly  U ) )  =  ( Base `  W
) )
4035, 39feq23d 5747 . . . . . 6  |-  ( ph  ->  ( A : R --> ( Base `  ( 1o mPoly  U ) )  <->  A :
( Base `  (Scalar `  W
) ) --> ( Base `  W ) ) )
4127, 40mpbird 236 . . . . 5  |-  ( ph  ->  A : R --> ( Base `  ( 1o mPoly  U )
) )
42 evls1sca.x . . . . 5  |-  ( ph  ->  X  e.  R )
4341, 42ffvelrnd 6044 . . . 4  |-  ( ph  ->  ( A `  X
)  e.  ( Base `  ( 1o mPoly  U )
) )
44 fvco3 5964 . . . 4  |-  ( ( ( ( 1o evalSub  S ) `
 R ) : ( Base `  ( 1o mPoly  U ) ) --> (
Base `  ( S  ^s  ( B  ^m  1o ) ) )  /\  ( A `  X )  e.  ( Base `  ( 1o mPoly  U ) ) )  ->  ( ( ( x  e.  ( B  ^m  ( B  ^m  1o ) )  |->  ( x  o.  ( y  e.  B  |->  ( 1o  X.  { y } ) ) ) )  o.  ( ( 1o evalSub  S ) `
 R ) ) `
 ( A `  X ) )  =  ( ( x  e.  ( B  ^m  ( B  ^m  1o ) ) 
|->  ( x  o.  (
y  e.  B  |->  ( 1o  X.  { y } ) ) ) ) `  ( ( ( 1o evalSub  S ) `  R ) `  ( A `  X )
) ) )
4515, 43, 44syl2anc 666 . . 3  |-  ( ph  ->  ( ( ( x  e.  ( B  ^m  ( B  ^m  1o ) )  |->  ( x  o.  ( y  e.  B  |->  ( 1o  X.  {
y } ) ) ) )  o.  (
( 1o evalSub  S ) `  R ) ) `  ( A `  X ) )  =  ( ( x  e.  ( B  ^m  ( B  ^m  1o ) )  |->  ( x  o.  ( y  e.  B  |->  ( 1o  X.  { y } ) ) ) ) `  ( ( ( 1o evalSub  S ) `  R
) `  ( A `  X ) ) ) )
4616a1i 11 . . . . . . . 8  |-  ( ph  ->  A  =  (algSc `  W ) )
47 eqid 2423 . . . . . . . . 9  |-  (algSc `  W )  =  (algSc `  W )
4820, 47ply1ascl 18856 . . . . . . . 8  |-  (algSc `  W )  =  (algSc `  ( 1o mPoly  U )
)
4946, 48syl6eq 2480 . . . . . . 7  |-  ( ph  ->  A  =  (algSc `  ( 1o mPoly  U ) ) )
5049fveq1d 5889 . . . . . 6  |-  ( ph  ->  ( A `  X
)  =  ( (algSc `  ( 1o mPoly  U )
) `  X )
)
5150fveq2d 5891 . . . . 5  |-  ( ph  ->  ( ( ( 1o evalSub  S ) `  R
) `  ( A `  X ) )  =  ( ( ( 1o evalSub  S ) `  R
) `  ( (algSc `  ( 1o mPoly  U )
) `  X )
) )
52 eqid 2423 . . . . . 6  |-  (algSc `  ( 1o mPoly  U ) )  =  (algSc `  ( 1o mPoly  U ) )
535, 6, 7, 9, 52, 2, 3, 4, 42evlssca 18750 . . . . 5  |-  ( ph  ->  ( ( ( 1o evalSub  S ) `  R
) `  ( (algSc `  ( 1o mPoly  U )
) `  X )
)  =  ( ( B  ^m  1o )  X.  { X }
) )
5451, 53eqtrd 2464 . . . 4  |-  ( ph  ->  ( ( ( 1o evalSub  S ) `  R
) `  ( A `  X ) )  =  ( ( B  ^m  1o )  X.  { X } ) )
5554fveq2d 5891 . . 3  |-  ( ph  ->  ( ( x  e.  ( B  ^m  ( B  ^m  1o ) ) 
|->  ( x  o.  (
y  e.  B  |->  ( 1o  X.  { y } ) ) ) ) `  ( ( ( 1o evalSub  S ) `  R ) `  ( A `  X )
) )  =  ( ( x  e.  ( B  ^m  ( B  ^m  1o ) ) 
|->  ( x  o.  (
y  e.  B  |->  ( 1o  X.  { y } ) ) ) ) `  ( ( B  ^m  1o )  X.  { X }
) ) )
56 eqidd 2424 . . . . 5  |-  ( ph  ->  ( x  e.  ( B  ^m  ( B  ^m  1o ) ) 
|->  ( x  o.  (
y  e.  B  |->  ( 1o  X.  { y } ) ) ) )  =  ( x  e.  ( B  ^m  ( B  ^m  1o ) )  |->  ( x  o.  ( y  e.  B  |->  ( 1o  X.  {
y } ) ) ) ) )
57 coeq1 5017 . . . . . 6  |-  ( x  =  ( ( B  ^m  1o )  X. 
{ X } )  ->  ( x  o.  ( y  e.  B  |->  ( 1o  X.  {
y } ) ) )  =  ( ( ( B  ^m  1o )  X.  { X }
)  o.  ( y  e.  B  |->  ( 1o 
X.  { y } ) ) ) )
5857adantl 468 . . . . 5  |-  ( (
ph  /\  x  =  ( ( B  ^m  1o )  X.  { X } ) )  -> 
( x  o.  (
y  e.  B  |->  ( 1o  X.  { y } ) ) )  =  ( ( ( B  ^m  1o )  X.  { X }
)  o.  ( y  e.  B  |->  ( 1o 
X.  { y } ) ) ) )
5929, 42sseldd 3471 . . . . . . 7  |-  ( ph  ->  X  e.  B )
60 fconst6g 5795 . . . . . . 7  |-  ( X  e.  B  ->  (
( B  ^m  1o )  X.  { X }
) : ( B  ^m  1o ) --> B )
6159, 60syl 17 . . . . . 6  |-  ( ph  ->  ( ( B  ^m  1o )  X.  { X } ) : ( B  ^m  1o ) --> B )
62 fvex 5897 . . . . . . . . 9  |-  ( Base `  S )  e.  _V
639, 62eqeltri 2508 . . . . . . . 8  |-  B  e. 
_V
6463a1i 11 . . . . . . 7  |-  ( ph  ->  B  e.  _V )
65 ovex 6339 . . . . . . . 8  |-  ( B  ^m  1o )  e. 
_V
6665a1i 11 . . . . . . 7  |-  ( ph  ->  ( B  ^m  1o )  e.  _V )
6764, 66elmapd 7503 . . . . . 6  |-  ( ph  ->  ( ( ( B  ^m  1o )  X. 
{ X } )  e.  ( B  ^m  ( B  ^m  1o ) )  <->  ( ( B  ^m  1o )  X. 
{ X } ) : ( B  ^m  1o ) --> B ) )
6861, 67mpbird 236 . . . . 5  |-  ( ph  ->  ( ( B  ^m  1o )  X.  { X } )  e.  ( B  ^m  ( B  ^m  1o ) ) )
69 snex 4668 . . . . . . . 8  |-  { X }  e.  _V
7065, 69xpex 6615 . . . . . . 7  |-  ( ( B  ^m  1o )  X.  { X }
)  e.  _V
7170a1i 11 . . . . . 6  |-  ( ph  ->  ( ( B  ^m  1o )  X.  { X } )  e.  _V )
72 mptexg 6156 . . . . . . 7  |-  ( B  e.  _V  ->  (
y  e.  B  |->  ( 1o  X.  { y } ) )  e. 
_V )
7364, 72syl 17 . . . . . 6  |-  ( ph  ->  ( y  e.  B  |->  ( 1o  X.  {
y } ) )  e.  _V )
74 coexg 6764 . . . . . 6  |-  ( ( ( ( B  ^m  1o )  X.  { X } )  e.  _V  /\  ( y  e.  B  |->  ( 1o  X.  {
y } ) )  e.  _V )  -> 
( ( ( B  ^m  1o )  X. 
{ X } )  o.  ( y  e.  B  |->  ( 1o  X.  { y } ) ) )  e.  _V )
7571, 73, 74syl2anc 666 . . . . 5  |-  ( ph  ->  ( ( ( B  ^m  1o )  X. 
{ X } )  o.  ( y  e.  B  |->  ( 1o  X.  { y } ) ) )  e.  _V )
7656, 58, 68, 75fvmptd 5976 . . . 4  |-  ( ph  ->  ( ( x  e.  ( B  ^m  ( B  ^m  1o ) ) 
|->  ( x  o.  (
y  e.  B  |->  ( 1o  X.  { y } ) ) ) ) `  ( ( B  ^m  1o )  X.  { X }
) )  =  ( ( ( B  ^m  1o )  X.  { X } )  o.  (
y  e.  B  |->  ( 1o  X.  { y } ) ) ) )
77 fconst6g 5795 . . . . . . 7  |-  ( y  e.  B  ->  ( 1o  X.  { y } ) : 1o --> B )
7877adantl 468 . . . . . 6  |-  ( (
ph  /\  y  e.  B )  ->  ( 1o  X.  { y } ) : 1o --> B )
7963, 1pm3.2i 457 . . . . . . . 8  |-  ( B  e.  _V  /\  1o  e.  On )
8079a1i 11 . . . . . . 7  |-  ( (
ph  /\  y  e.  B )  ->  ( B  e.  _V  /\  1o  e.  On ) )
81 elmapg 7502 . . . . . . 7  |-  ( ( B  e.  _V  /\  1o  e.  On )  -> 
( ( 1o  X.  { y } )  e.  ( B  ^m  1o )  <->  ( 1o  X.  { y } ) : 1o --> B ) )
8280, 81syl 17 . . . . . 6  |-  ( (
ph  /\  y  e.  B )  ->  (
( 1o  X.  {
y } )  e.  ( B  ^m  1o ) 
<->  ( 1o  X.  {
y } ) : 1o --> B ) )
8378, 82mpbird 236 . . . . 5  |-  ( (
ph  /\  y  e.  B )  ->  ( 1o  X.  { y } )  e.  ( B  ^m  1o ) )
84 eqidd 2424 . . . . 5  |-  ( ph  ->  ( y  e.  B  |->  ( 1o  X.  {
y } ) )  =  ( y  e.  B  |->  ( 1o  X.  { y } ) ) )
85 fconstmpt 4903 . . . . . 6  |-  ( ( B  ^m  1o )  X.  { X }
)  =  ( z  e.  ( B  ^m  1o )  |->  X )
8685a1i 11 . . . . 5  |-  ( ph  ->  ( ( B  ^m  1o )  X.  { X } )  =  ( z  e.  ( B  ^m  1o )  |->  X ) )
87 eqidd 2424 . . . . 5  |-  ( z  =  ( 1o  X.  { y } )  ->  X  =  X )
8883, 84, 86, 87fmptco 6077 . . . 4  |-  ( ph  ->  ( ( ( B  ^m  1o )  X. 
{ X } )  o.  ( y  e.  B  |->  ( 1o  X.  { y } ) ) )  =  ( y  e.  B  |->  X ) )
8976, 88eqtrd 2464 . . 3  |-  ( ph  ->  ( ( x  e.  ( B  ^m  ( B  ^m  1o ) ) 
|->  ( x  o.  (
y  e.  B  |->  ( 1o  X.  { y } ) ) ) ) `  ( ( B  ^m  1o )  X.  { X }
) )  =  ( y  e.  B  |->  X ) )
9045, 55, 893eqtrd 2468 . 2  |-  ( ph  ->  ( ( ( x  e.  ( B  ^m  ( B  ^m  1o ) )  |->  ( x  o.  ( y  e.  B  |->  ( 1o  X.  {
y } ) ) ) )  o.  (
( 1o evalSub  S ) `  R ) ) `  ( A `  X ) )  =  ( y  e.  B  |->  X ) )
91 elpwg 3995 . . . . . 6  |-  ( R  e.  (SubRing `  S
)  ->  ( R  e.  ~P B  <->  R  C_  B
) )
9228, 91mpbird 236 . . . . 5  |-  ( R  e.  (SubRing `  S
)  ->  R  e.  ~P B )
934, 92syl 17 . . . 4  |-  ( ph  ->  R  e.  ~P B
)
94 evls1sca.q . . . . 5  |-  Q  =  ( S evalSub1  R )
95 eqid 2423 . . . . 5  |-  ( 1o evalSub  S )  =  ( 1o evalSub  S )
9694, 95, 9evls1fval 18913 . . . 4  |-  ( ( S  e.  CRing  /\  R  e.  ~P B )  ->  Q  =  ( (
x  e.  ( B  ^m  ( B  ^m  1o ) )  |->  ( x  o.  ( y  e.  B  |->  ( 1o  X.  { y } ) ) ) )  o.  ( ( 1o evalSub  S ) `
 R ) ) )
973, 93, 96syl2anc 666 . . 3  |-  ( ph  ->  Q  =  ( ( x  e.  ( B  ^m  ( B  ^m  1o ) )  |->  ( x  o.  ( y  e.  B  |->  ( 1o  X.  { y } ) ) ) )  o.  ( ( 1o evalSub  S ) `
 R ) ) )
9897fveq1d 5889 . 2  |-  ( ph  ->  ( Q `  ( A `  X )
)  =  ( ( ( x  e.  ( B  ^m  ( B  ^m  1o ) ) 
|->  ( x  o.  (
y  e.  B  |->  ( 1o  X.  { y } ) ) ) )  o.  ( ( 1o evalSub  S ) `  R
) ) `  ( A `  X )
) )
99 fconstmpt 4903 . . 3  |-  ( B  X.  { X }
)  =  ( y  e.  B  |->  X )
10099a1i 11 . 2  |-  ( ph  ->  ( B  X.  { X } )  =  ( y  e.  B  |->  X ) )
10190, 98, 1003eqtr4d 2474 1  |-  ( ph  ->  ( Q `  ( A `  X )
)  =  ( B  X.  { X }
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1438    e. wcel 1873   _Vcvv 3085    C_ wss 3442   ~Pcpw 3987   {csn 4004    |-> cmpt 4488    X. cxp 4857    o. ccom 4863   Oncon0 5448   -->wf 5603   ` cfv 5607  (class class class)co 6311   1oc1o 7192    ^m cmap 7489   Basecbs 15126   ↾s cress 15127  Scalarcsca 15198    ^s cpws 15350   Ringcrg 17785   CRingccrg 17786   RingHom crh 17945  SubRingcsubrg 18009   LModclmod 18096  algSccascl 18540   mPoly cmpl 18582   evalSub ces 18732  PwSer1cps1 18773  Poly1cpl1 18775   evalSub1 ces1 18907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-8 1875  ax-9 1877  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-rep 4542  ax-sep 4552  ax-nul 4561  ax-pow 4608  ax-pr 4666  ax-un 6603  ax-inf2 8161  ax-cnex 9608  ax-resscn 9609  ax-1cn 9610  ax-icn 9611  ax-addcl 9612  ax-addrcl 9613  ax-mulcl 9614  ax-mulrcl 9615  ax-mulcom 9616  ax-addass 9617  ax-mulass 9618  ax-distr 9619  ax-i2m1 9620  ax-1ne0 9621  ax-1rid 9622  ax-rnegex 9623  ax-rrecex 9624  ax-cnre 9625  ax-pre-lttri 9626  ax-pre-lttrn 9627  ax-pre-ltadd 9628  ax-pre-mulgt0 9629
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3087  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3918  df-pw 3989  df-sn 4005  df-pr 4007  df-tp 4009  df-op 4011  df-uni 4226  df-int 4262  df-iun 4307  df-iin 4308  df-br 4430  df-opab 4489  df-mpt 4490  df-tr 4525  df-eprel 4770  df-id 4774  df-po 4780  df-so 4781  df-fr 4818  df-se 4819  df-we 4820  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-pred 5405  df-ord 5451  df-on 5452  df-lim 5453  df-suc 5454  df-iota 5571  df-fun 5609  df-fn 5610  df-f 5611  df-f1 5612  df-fo 5613  df-f1o 5614  df-fv 5615  df-isom 5616  df-riota 6273  df-ov 6314  df-oprab 6315  df-mpt2 6316  df-of 6551  df-ofr 6552  df-om 6713  df-1st 6813  df-2nd 6814  df-supp 6932  df-wrecs 7045  df-recs 7107  df-rdg 7145  df-1o 7199  df-2o 7200  df-oadd 7203  df-er 7380  df-map 7491  df-pm 7492  df-ixp 7540  df-en 7587  df-dom 7588  df-sdom 7589  df-fin 7590  df-fsupp 7899  df-sup 7971  df-oi 8040  df-card 8387  df-pnf 9690  df-mnf 9691  df-xr 9692  df-ltxr 9693  df-le 9694  df-sub 9875  df-neg 9876  df-nn 10623  df-2 10681  df-3 10682  df-4 10683  df-5 10684  df-6 10685  df-7 10686  df-8 10687  df-9 10688  df-10 10689  df-n0 10883  df-z 10951  df-dec 11065  df-uz 11173  df-fz 11798  df-fzo 11929  df-seq 12226  df-hash 12528  df-struct 15128  df-ndx 15129  df-slot 15130  df-base 15131  df-sets 15132  df-ress 15133  df-plusg 15208  df-mulr 15209  df-sca 15211  df-vsca 15212  df-ip 15213  df-tset 15214  df-ple 15215  df-ds 15217  df-hom 15219  df-cco 15220  df-0g 15345  df-gsum 15346  df-prds 15351  df-pws 15353  df-mre 15497  df-mrc 15498  df-acs 15500  df-mgm 16493  df-sgrp 16532  df-mnd 16542  df-mhm 16587  df-submnd 16588  df-grp 16678  df-minusg 16679  df-sbg 16680  df-mulg 16681  df-subg 16819  df-ghm 16886  df-cntz 16976  df-cmn 17437  df-abl 17438  df-mgp 17729  df-ur 17741  df-srg 17745  df-ring 17787  df-cring 17788  df-rnghom 17948  df-subrg 18011  df-lmod 18098  df-lss 18161  df-lsp 18200  df-assa 18541  df-asp 18542  df-ascl 18543  df-psr 18585  df-mvr 18586  df-mpl 18587  df-opsr 18589  df-evls 18734  df-psr1 18778  df-ply1 18780  df-evls1 18909
This theorem is referenced by:  evls1scasrng  18932
  Copyright terms: Public domain W3C validator