| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mhphf3.q |
|- Q = ( ( I evalSub S ) ` R ) |
| 2 |
|
mhphf3.h |
|- H = ( I mHomP U ) |
| 3 |
|
mhphf3.u |
|- U = ( S |`s R ) |
| 4 |
|
mhphf3.k |
|- K = ( Base ` S ) |
| 5 |
|
mhphf3.f |
|- F = ( S freeLMod I ) |
| 6 |
|
mhphf3.m |
|- M = ( Base ` F ) |
| 7 |
|
mhphf3.b |
|- .xb = ( .s ` F ) |
| 8 |
|
mhphf3.x |
|- .x. = ( .r ` S ) |
| 9 |
|
mhphf3.e |
|- .^ = ( .g ` ( mulGrp ` S ) ) |
| 10 |
|
mhphf3.s |
|- ( ph -> S e. CRing ) |
| 11 |
|
mhphf3.r |
|- ( ph -> R e. ( SubRing ` S ) ) |
| 12 |
|
mhphf3.l |
|- ( ph -> L e. R ) |
| 13 |
|
mhphf3.p |
|- ( ph -> X e. ( H ` N ) ) |
| 14 |
|
mhphf3.a |
|- ( ph -> A e. M ) |
| 15 |
|
reldmmhp |
|- Rel dom mHomP |
| 16 |
15 2 13
|
elfvov1 |
|- ( ph -> I e. _V ) |
| 17 |
4
|
subrgss |
|- ( R e. ( SubRing ` S ) -> R C_ K ) |
| 18 |
11 17
|
syl |
|- ( ph -> R C_ K ) |
| 19 |
18 12
|
sseldd |
|- ( ph -> L e. K ) |
| 20 |
5 6 4 16 19 14 7 8
|
frlmvscafval |
|- ( ph -> ( L .xb A ) = ( ( I X. { L } ) oF .x. A ) ) |
| 21 |
20
|
fveq2d |
|- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) ) |
| 22 |
5 4 6
|
frlmbasmap |
|- ( ( I e. _V /\ A e. M ) -> A e. ( K ^m I ) ) |
| 23 |
16 14 22
|
syl2anc |
|- ( ph -> A e. ( K ^m I ) ) |
| 24 |
1 2 3 4 8 9 10 11 12 13 23
|
mhphf |
|- ( ph -> ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) ) |
| 25 |
21 24
|
eqtrd |
|- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) ) |