| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mpfsubrg.q |
|- Q = ran ( ( I evalSub S ) ` R ) |
| 2 |
|
mpff.b |
|- B = ( Base ` S ) |
| 3 |
2
|
eqcomi |
|- ( Base ` S ) = B |
| 4 |
3
|
oveq1i |
|- ( ( Base ` S ) ^m I ) = ( B ^m I ) |
| 5 |
4
|
oveq2i |
|- ( S ^s ( ( Base ` S ) ^m I ) ) = ( S ^s ( B ^m I ) ) |
| 6 |
|
eqid |
|- ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) = ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) |
| 7 |
1
|
mpfrcl |
|- ( F e. Q -> ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) ) |
| 8 |
7
|
simp2d |
|- ( F e. Q -> S e. CRing ) |
| 9 |
|
ovexd |
|- ( F e. Q -> ( B ^m I ) e. _V ) |
| 10 |
1
|
mpfsubrg |
|- ( ( I e. _V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) ) |
| 11 |
6
|
subrgss |
|- ( Q e. ( SubRing ` ( S ^s ( ( Base ` S ) ^m I ) ) ) -> Q C_ ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) ) |
| 12 |
7 10 11
|
3syl |
|- ( F e. Q -> Q C_ ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) ) |
| 13 |
|
id |
|- ( F e. Q -> F e. Q ) |
| 14 |
12 13
|
sseldd |
|- ( F e. Q -> F e. ( Base ` ( S ^s ( ( Base ` S ) ^m I ) ) ) ) |
| 15 |
5 2 6 8 9 14
|
pwselbas |
|- ( F e. Q -> F : ( B ^m I ) --> B ) |