Step |
Hyp |
Ref |
Expression |
1 |
|
rhmpsr1.p |
|- P = ( PwSer1 ` R ) |
2 |
|
rhmpsr1.q |
|- Q = ( PwSer1 ` S ) |
3 |
|
rhmpsr1.b |
|- B = ( Base ` P ) |
4 |
|
rhmpsr1.f |
|- F = ( p e. B |-> ( H o. p ) ) |
5 |
|
rhmpsr1.h |
|- ( ph -> H e. ( R RingHom S ) ) |
6 |
|
eqid |
|- ( 1o mPwSer R ) = ( 1o mPwSer R ) |
7 |
|
eqid |
|- ( 1o mPwSer S ) = ( 1o mPwSer S ) |
8 |
1 3 6
|
psr1bas2 |
|- B = ( Base ` ( 1o mPwSer R ) ) |
9 |
|
1oex |
|- 1o e. _V |
10 |
9
|
a1i |
|- ( ph -> 1o e. _V ) |
11 |
6 7 8 4 10 5
|
rhmpsr |
|- ( ph -> F e. ( ( 1o mPwSer R ) RingHom ( 1o mPwSer S ) ) ) |
12 |
|
eqid |
|- ( Base ` P ) = ( Base ` P ) |
13 |
1 12 6
|
psr1bas2 |
|- ( Base ` P ) = ( Base ` ( 1o mPwSer R ) ) |
14 |
13
|
a1i |
|- ( ph -> ( Base ` P ) = ( Base ` ( 1o mPwSer R ) ) ) |
15 |
|
eqid |
|- ( Base ` Q ) = ( Base ` Q ) |
16 |
2 15 7
|
psr1bas2 |
|- ( Base ` Q ) = ( Base ` ( 1o mPwSer S ) ) |
17 |
16
|
a1i |
|- ( ph -> ( Base ` Q ) = ( Base ` ( 1o mPwSer S ) ) ) |
18 |
|
eqidd |
|- ( ph -> ( Base ` P ) = ( Base ` P ) ) |
19 |
|
eqidd |
|- ( ph -> ( Base ` Q ) = ( Base ` Q ) ) |
20 |
|
eqid |
|- ( +g ` P ) = ( +g ` P ) |
21 |
1 6 20
|
psr1plusg |
|- ( +g ` P ) = ( +g ` ( 1o mPwSer R ) ) |
22 |
21
|
eqcomi |
|- ( +g ` ( 1o mPwSer R ) ) = ( +g ` P ) |
23 |
22
|
a1i |
|- ( ( ph /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( +g ` ( 1o mPwSer R ) ) = ( +g ` P ) ) |
24 |
23
|
oveqd |
|- ( ( ph /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( +g ` ( 1o mPwSer R ) ) y ) = ( x ( +g ` P ) y ) ) |
25 |
|
eqid |
|- ( +g ` Q ) = ( +g ` Q ) |
26 |
2 7 25
|
psr1plusg |
|- ( +g ` Q ) = ( +g ` ( 1o mPwSer S ) ) |
27 |
26
|
eqcomi |
|- ( +g ` ( 1o mPwSer S ) ) = ( +g ` Q ) |
28 |
27
|
a1i |
|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( +g ` ( 1o mPwSer S ) ) = ( +g ` Q ) ) |
29 |
28
|
oveqd |
|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( x ( +g ` ( 1o mPwSer S ) ) y ) = ( x ( +g ` Q ) y ) ) |
30 |
|
eqid |
|- ( .r ` P ) = ( .r ` P ) |
31 |
1 6 30
|
psr1mulr |
|- ( .r ` P ) = ( .r ` ( 1o mPwSer R ) ) |
32 |
31
|
eqcomi |
|- ( .r ` ( 1o mPwSer R ) ) = ( .r ` P ) |
33 |
32
|
a1i |
|- ( ( ph /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( .r ` ( 1o mPwSer R ) ) = ( .r ` P ) ) |
34 |
33
|
oveqd |
|- ( ( ph /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( .r ` ( 1o mPwSer R ) ) y ) = ( x ( .r ` P ) y ) ) |
35 |
|
eqid |
|- ( .r ` Q ) = ( .r ` Q ) |
36 |
2 7 35
|
psr1mulr |
|- ( .r ` Q ) = ( .r ` ( 1o mPwSer S ) ) |
37 |
36
|
eqcomi |
|- ( .r ` ( 1o mPwSer S ) ) = ( .r ` Q ) |
38 |
37
|
a1i |
|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( .r ` ( 1o mPwSer S ) ) = ( .r ` Q ) ) |
39 |
38
|
oveqd |
|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( x ( .r ` ( 1o mPwSer S ) ) y ) = ( x ( .r ` Q ) y ) ) |
40 |
14 17 18 19 24 29 34 39
|
rhmpropd |
|- ( ph -> ( ( 1o mPwSer R ) RingHom ( 1o mPwSer S ) ) = ( P RingHom Q ) ) |
41 |
11 40
|
eleqtrd |
|- ( ph -> F e. ( P RingHom Q ) ) |