Step |
Hyp |
Ref |
Expression |
1 |
|
rhmply1vr1.p |
|- P = ( Poly1 ` R ) |
2 |
|
rhmply1vr1.q |
|- Q = ( Poly1 ` S ) |
3 |
|
rhmply1vr1.b |
|- B = ( Base ` P ) |
4 |
|
rhmply1vr1.f |
|- F = ( p e. B |-> ( H o. p ) ) |
5 |
|
rhmply1vr1.x |
|- X = ( var1 ` R ) |
6 |
|
rhmply1vr1.y |
|- Y = ( var1 ` S ) |
7 |
|
rhmply1vr1.h |
|- ( ph -> H e. ( R RingHom S ) ) |
8 |
|
coeq2 |
|- ( p = X -> ( H o. p ) = ( H o. X ) ) |
9 |
|
rhmrcl1 |
|- ( H e. ( R RingHom S ) -> R e. Ring ) |
10 |
7 9
|
syl |
|- ( ph -> R e. Ring ) |
11 |
5 1 3
|
vr1cl |
|- ( R e. Ring -> X e. B ) |
12 |
10 11
|
syl |
|- ( ph -> X e. B ) |
13 |
5
|
fvexi |
|- X e. _V |
14 |
13
|
a1i |
|- ( ph -> X e. _V ) |
15 |
7 14
|
coexd |
|- ( ph -> ( H o. X ) e. _V ) |
16 |
4 8 12 15
|
fvmptd3 |
|- ( ph -> ( F ` X ) = ( H o. X ) ) |
17 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
18 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
19 |
17 18
|
rhmf |
|- ( H e. ( R RingHom S ) -> H : ( Base ` R ) --> ( Base ` S ) ) |
20 |
7 19
|
syl |
|- ( ph -> H : ( Base ` R ) --> ( Base ` S ) ) |
21 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
22 |
17 21
|
ringidcl |
|- ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) ) |
23 |
10 22
|
syl |
|- ( ph -> ( 1r ` R ) e. ( Base ` R ) ) |
24 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
25 |
17 24
|
ring0cl |
|- ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) ) |
26 |
10 25
|
syl |
|- ( ph -> ( 0g ` R ) e. ( Base ` R ) ) |
27 |
23 26
|
ifcld |
|- ( ph -> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) ) |
28 |
27
|
adantr |
|- ( ( ph /\ f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } ) -> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) ) |
29 |
20 28
|
cofmpt |
|- ( ph -> ( H o. ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> ( H ` if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) |
30 |
|
fvif |
|- ( H ` if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( H ` ( 1r ` R ) ) , ( H ` ( 0g ` R ) ) ) |
31 |
|
eqid |
|- ( 1r ` S ) = ( 1r ` S ) |
32 |
21 31
|
rhm1 |
|- ( H e. ( R RingHom S ) -> ( H ` ( 1r ` R ) ) = ( 1r ` S ) ) |
33 |
7 32
|
syl |
|- ( ph -> ( H ` ( 1r ` R ) ) = ( 1r ` S ) ) |
34 |
|
rhmghm |
|- ( H e. ( R RingHom S ) -> H e. ( R GrpHom S ) ) |
35 |
|
eqid |
|- ( 0g ` S ) = ( 0g ` S ) |
36 |
24 35
|
ghmid |
|- ( H e. ( R GrpHom S ) -> ( H ` ( 0g ` R ) ) = ( 0g ` S ) ) |
37 |
7 34 36
|
3syl |
|- ( ph -> ( H ` ( 0g ` R ) ) = ( 0g ` S ) ) |
38 |
33 37
|
ifeq12d |
|- ( ph -> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( H ` ( 1r ` R ) ) , ( H ` ( 0g ` R ) ) ) = if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` S ) , ( 0g ` S ) ) ) |
39 |
30 38
|
eqtrid |
|- ( ph -> ( H ` if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` S ) , ( 0g ` S ) ) ) |
40 |
39
|
mpteq2dv |
|- ( ph -> ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> ( H ` if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` S ) , ( 0g ` S ) ) ) ) |
41 |
29 40
|
eqtrd |
|- ( ph -> ( H o. ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` S ) , ( 0g ` S ) ) ) ) |
42 |
|
eqid |
|- ( 1o mVar R ) = ( 1o mVar R ) |
43 |
|
eqid |
|- { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |
44 |
|
1oex |
|- 1o e. _V |
45 |
44
|
a1i |
|- ( ph -> 1o e. _V ) |
46 |
|
0lt1o |
|- (/) e. 1o |
47 |
46
|
a1i |
|- ( ph -> (/) e. 1o ) |
48 |
42 43 24 21 45 10 47
|
mvrval |
|- ( ph -> ( ( 1o mVar R ) ` (/) ) = ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) |
49 |
48
|
coeq2d |
|- ( ph -> ( H o. ( ( 1o mVar R ) ` (/) ) ) = ( H o. ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) |
50 |
|
eqid |
|- ( 1o mVar S ) = ( 1o mVar S ) |
51 |
|
rhmrcl2 |
|- ( H e. ( R RingHom S ) -> S e. Ring ) |
52 |
7 51
|
syl |
|- ( ph -> S e. Ring ) |
53 |
50 43 35 31 45 52 47
|
mvrval |
|- ( ph -> ( ( 1o mVar S ) ` (/) ) = ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` S ) , ( 0g ` S ) ) ) ) |
54 |
41 49 53
|
3eqtr4d |
|- ( ph -> ( H o. ( ( 1o mVar R ) ` (/) ) ) = ( ( 1o mVar S ) ` (/) ) ) |
55 |
5
|
vr1val |
|- X = ( ( 1o mVar R ) ` (/) ) |
56 |
55
|
coeq2i |
|- ( H o. X ) = ( H o. ( ( 1o mVar R ) ` (/) ) ) |
57 |
6
|
vr1val |
|- Y = ( ( 1o mVar S ) ` (/) ) |
58 |
54 56 57
|
3eqtr4g |
|- ( ph -> ( H o. X ) = Y ) |
59 |
16 58
|
eqtrd |
|- ( ph -> ( F ` X ) = Y ) |