Metamath Proof Explorer

Theorem rhmcomulmpl

Description: Show that the ring homomorphism in rhmmpl preserves multiplication. (Contributed by SN, 8-Feb-2025)

Ref Expression
Hypotheses rhmcomulmpl.p 
|- P = ( I mPoly R )
rhmcomulmpl.q 
|- Q = ( I mPoly S )
rhmcomulmpl.b 
|- B = ( Base ` P )
rhmcomulmpl.c 
|- C = ( Base ` Q )
rhmcomulmpl.1 
|- .x. = ( .r ` P )
rhmcomulmpl.2 
|- .xb = ( .r ` Q )
rhmcomulmpl.h 
|- ( ph -> H e. ( R RingHom S ) )
rhmcomulmpl.f 
|- ( ph -> F e. B )
rhmcomulmpl.g 
|- ( ph -> G e. B )
Assertion rhmcomulmpl 
|- ( ph -> ( H o. ( F .x. G ) ) = ( ( H o. F ) .xb ( H o. G ) ) )

Proof

Step Hyp Ref Expression
1 rhmcomulmpl.p 
 |-  P = ( I mPoly R )
2 rhmcomulmpl.q 
 |-  Q = ( I mPoly S )
3 rhmcomulmpl.b 
 |-  B = ( Base ` P )
4 rhmcomulmpl.c 
 |-  C = ( Base ` Q )
5 rhmcomulmpl.1 
 |-  .x. = ( .r ` P )
6 rhmcomulmpl.2 
 |-  .xb = ( .r ` Q )
7 rhmcomulmpl.h 
 |-  ( ph -> H e. ( R RingHom S ) )
8 rhmcomulmpl.f 
 |-  ( ph -> F e. B )
9 rhmcomulmpl.g 
 |-  ( ph -> G e. B )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 eqid 
 |-  ( Base ` S ) = ( Base ` S )
12 10 11 rhmf 
 |-  ( H e. ( R RingHom S ) -> H : ( Base ` R ) --> ( Base ` S ) )
13 7 12 syl 
 |-  ( ph -> H : ( Base ` R ) --> ( Base ` S ) )
14 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
15 rhmrcl1 
 |-  ( H e. ( R RingHom S ) -> R e. Ring )
16 7 15 syl 
 |-  ( ph -> R e. Ring )
17 1 10 3 14 8 mplelf 
 |-  ( ph -> F : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
18 1 10 3 14 9 mplelf 
 |-  ( ph -> G : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
19 14 16 17 18 rhmpsrlem2 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( R gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) e. ( Base ` R ) )
20 13 19 cofmpt 
 |-  ( ph -> ( H o. ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( R gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) ) ) = ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( H ` ( R gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) ) ) )
21 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
22 16 ringcmnd 
 |-  ( ph -> R e. CMnd )
23 22 adantr 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> R e. CMnd )
24 rhmrcl2 
 |-  ( H e. ( R RingHom S ) -> S e. Ring )
25 7 24 syl 
 |-  ( ph -> S e. Ring )
26 25 ringgrpd 
 |-  ( ph -> S e. Grp )
27 26 grpmndd 
 |-  ( ph -> S e. Mnd )
28 27 adantr 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> S e. Mnd )
29 ovex 
 |-  ( NN0 ^m I ) e. _V
30 29 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
31 30 rabex 
 |-  { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } e. _V
32 31 a1i 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } e. _V )
33 rhmghm 
 |-  ( H e. ( R RingHom S ) -> H e. ( R GrpHom S ) )
34 ghmmhm 
 |-  ( H e. ( R GrpHom S ) -> H e. ( R MndHom S ) )
35 7 33 34 3syl 
 |-  ( ph -> H e. ( R MndHom S ) )
36 35 adantr 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> H e. ( R MndHom S ) )
37 eqid 
 |-  ( .r ` R ) = ( .r ` R )
38 16 ad2antrr 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> R e. Ring )
39 elrabi 
 |-  ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } -> d e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
40 17 ffvelcdmda 
 |-  ( ( ph /\ d e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( F ` d ) e. ( Base ` R ) )
41 39 40 sylan2 
 |-  ( ( ph /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( F ` d ) e. ( Base ` R ) )
42 41 adantlr 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( F ` d ) e. ( Base ` R ) )
43 18 ad2antrr 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> G : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
44 eqid 
 |-  { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } = { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k }
45 14 44 psrbagconcl 
 |-  ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( k oF - d ) e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } )
46 elrabi 
 |-  ( ( k oF - d ) e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } -> ( k oF - d ) e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
47 45 46 syl 
 |-  ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( k oF - d ) e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
48 47 adantll 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( k oF - d ) e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
49 43 48 ffvelcdmd 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( G ` ( k oF - d ) ) e. ( Base ` R ) )
50 10 37 38 42 49 ringcld 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) e. ( Base ` R ) )
51 14 16 17 18 rhmpsrlem1 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) finSupp ( 0g ` R ) )
52 10 21 23 28 32 36 50 51 gsummptmhm 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( S gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( H ` ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) ) = ( H ` ( R gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) ) )
53 7 ad2antrr 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> H e. ( R RingHom S ) )
54 eqid 
 |-  ( .r ` S ) = ( .r ` S )
55 10 37 54 rhmmul 
 |-  ( ( H e. ( R RingHom S ) /\ ( F ` d ) e. ( Base ` R ) /\ ( G ` ( k oF - d ) ) e. ( Base ` R ) ) -> ( H ` ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) = ( ( H ` ( F ` d ) ) ( .r ` S ) ( H ` ( G ` ( k oF - d ) ) ) ) )
56 53 42 49 55 syl3anc 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( H ` ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) = ( ( H ` ( F ` d ) ) ( .r ` S ) ( H ` ( G ` ( k oF - d ) ) ) ) )
57 17 ad2antrr 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> F : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
58 39 adantl 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> d e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
59 57 58 fvco3d 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( ( H o. F ) ` d ) = ( H ` ( F ` d ) ) )
60 43 48 fvco3d 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( ( H o. G ) ` ( k oF - d ) ) = ( H ` ( G ` ( k oF - d ) ) ) )
61 59 60 oveq12d 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( ( ( H o. F ) ` d ) ( .r ` S ) ( ( H o. G ) ` ( k oF - d ) ) ) = ( ( H ` ( F ` d ) ) ( .r ` S ) ( H ` ( G ` ( k oF - d ) ) ) ) )
62 56 61 eqtr4d 
 |-  ( ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) /\ d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } ) -> ( H ` ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) = ( ( ( H o. F ) ` d ) ( .r ` S ) ( ( H o. G ) ` ( k oF - d ) ) ) )
63 62 mpteq2dva 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( H ` ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) = ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( ( H o. F ) ` d ) ( .r ` S ) ( ( H o. G ) ` ( k oF - d ) ) ) ) )
64 63 oveq2d 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( S gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( H ` ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) ) = ( S gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( ( H o. F ) ` d ) ( .r ` S ) ( ( H o. G ) ` ( k oF - d ) ) ) ) ) )
65 52 64 eqtr3d 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> ( H ` ( R gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) ) = ( S gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( ( H o. F ) ` d ) ( .r ` S ) ( ( H o. G ) ` ( k oF - d ) ) ) ) ) )
66 65 mpteq2dva 
 |-  ( ph -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( H ` ( R gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) ) ) = ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( S gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( ( H o. F ) ` d ) ( .r ` S ) ( ( H o. G ) ` ( k oF - d ) ) ) ) ) ) )
67 20 66 eqtrd 
 |-  ( ph -> ( H o. ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( R gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) ) ) = ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( S gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( ( H o. F ) ` d ) ( .r ` S ) ( ( H o. G ) ` ( k oF - d ) ) ) ) ) ) )
68 1 3 37 5 14 8 9 mplmul 
 |-  ( ph -> ( F .x. G ) = ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( R gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) ) )
69 68 coeq2d 
 |-  ( ph -> ( H o. ( F .x. G ) ) = ( H o. ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( R gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( F ` d ) ( .r ` R ) ( G ` ( k oF - d ) ) ) ) ) ) ) )
70 1 2 3 4 35 8 mhmcompl 
 |-  ( ph -> ( H o. F ) e. C )
71 1 2 3 4 35 9 mhmcompl 
 |-  ( ph -> ( H o. G ) e. C )
72 2 4 54 6 14 70 71 mplmul 
 |-  ( ph -> ( ( H o. F ) .xb ( H o. G ) ) = ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> ( S gsum ( d e. { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } |-> ( ( ( H o. F ) ` d ) ( .r ` S ) ( ( H o. G ) ` ( k oF - d ) ) ) ) ) ) )
73 67 69 72 3eqtr4d 
 |-  ( ph -> ( H o. ( F .x. G ) ) = ( ( H o. F ) .xb ( H o. G ) ) )