Description: Well-behaved binary operation property of evalSub . (Contributed by Stefan O'Rear, 19-Mar-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | reldmevls | |- Rel dom evalSub |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-evls | |- evalSub = ( i e. _V , s e. CRing |-> [_ ( Base ` s ) / b ]_ ( r e. ( SubRing ` s ) |-> [_ ( i mPoly ( s |`s r ) ) / w ]_ ( iota_ f e. ( w RingHom ( s ^s ( b ^m i ) ) ) ( ( f o. ( algSc ` w ) ) = ( x e. r |-> ( ( b ^m i ) X. { x } ) ) /\ ( f o. ( i mVar ( s |`s r ) ) ) = ( x e. i |-> ( g e. ( b ^m i ) |-> ( g ` x ) ) ) ) ) ) ) |
|
| 2 | 1 | reldmmpo | |- Rel dom evalSub |