| Step |
Hyp |
Ref |
Expression |
| 1 |
|
evl1sca.o |
|- O = ( eval1 ` R ) |
| 2 |
|
evl1sca.p |
|- P = ( Poly1 ` R ) |
| 3 |
|
evl1sca.b |
|- B = ( Base ` R ) |
| 4 |
|
evl1sca.a |
|- A = ( algSc ` P ) |
| 5 |
|
evl1scad.u |
|- U = ( Base ` P ) |
| 6 |
|
evl1scad.1 |
|- ( ph -> R e. CRing ) |
| 7 |
|
evl1scad.2 |
|- ( ph -> X e. B ) |
| 8 |
|
evl1scad.3 |
|- ( ph -> Y e. B ) |
| 9 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
| 10 |
2 4 3 5
|
ply1sclf |
|- ( R e. Ring -> A : B --> U ) |
| 11 |
6 9 10
|
3syl |
|- ( ph -> A : B --> U ) |
| 12 |
11 7
|
ffvelcdmd |
|- ( ph -> ( A ` X ) e. U ) |
| 13 |
1 2 3 4
|
evl1sca |
|- ( ( R e. CRing /\ X e. B ) -> ( O ` ( A ` X ) ) = ( B X. { X } ) ) |
| 14 |
6 7 13
|
syl2anc |
|- ( ph -> ( O ` ( A ` X ) ) = ( B X. { X } ) ) |
| 15 |
14
|
fveq1d |
|- ( ph -> ( ( O ` ( A ` X ) ) ` Y ) = ( ( B X. { X } ) ` Y ) ) |
| 16 |
|
fvconst2g |
|- ( ( X e. B /\ Y e. B ) -> ( ( B X. { X } ) ` Y ) = X ) |
| 17 |
7 8 16
|
syl2anc |
|- ( ph -> ( ( B X. { X } ) ` Y ) = X ) |
| 18 |
15 17
|
eqtrd |
|- ( ph -> ( ( O ` ( A ` X ) ) ` Y ) = X ) |
| 19 |
12 18
|
jca |
|- ( ph -> ( ( A ` X ) e. U /\ ( ( O ` ( A ` X ) ) ` Y ) = X ) ) |