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.i 
|- ( ph -> I e. V )
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.i 
 |-  ( ph -> I e. V )
8 rhmcomulmpl.h 
 |-  ( ph -> H e. ( R RingHom S ) )
9 rhmcomulmpl.f 
 |-  ( ph -> F e. B )
10 rhmcomulmpl.g 
 |-  ( ph -> G e. B )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 eqid 
 |-  ( Base ` S ) = ( Base ` S )
13 11 12 rhmf 
 |-  ( H e. ( R RingHom S ) -> H : ( Base ` R ) --> ( Base ` S ) )
14 8 13 syl 
 |-  ( ph -> H : ( Base ` R ) --> ( Base ` S ) )
15 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
16 rhmrcl1 
 |-  ( H e. ( R RingHom S ) -> R e. Ring )
17 8 16 syl 
 |-  ( ph -> R e. Ring )
18 1 11 3 15 9 mplelf 
 |-  ( ph -> F : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
19 1 11 3 15 10 mplelf 
 |-  ( ph -> G : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
20 15 17 18 19 rhmmpllem2 
 |-  ( ( 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 ) )
21 14 20 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 ) ) ) ) ) ) ) )
22 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
23 17 ringcmnd 
 |-  ( ph -> R e. CMnd )
24 23 adantr 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> R e. CMnd )
25 rhmrcl2 
 |-  ( H e. ( R RingHom S ) -> S e. Ring )
26 8 25 syl 
 |-  ( ph -> S e. Ring )
27 26 ringgrpd 
 |-  ( ph -> S e. Grp )
28 27 grpmndd 
 |-  ( ph -> S e. Mnd )
29 28 adantr 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> S e. Mnd )
30 ovex 
 |-  ( NN0 ^m I ) e. _V
31 30 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
32 31 rabex 
 |-  { e e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } | e oR <_ k } e. _V
33 32 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 )
34 rhmghm 
 |-  ( H e. ( R RingHom S ) -> H e. ( R GrpHom S ) )
35 ghmmhm 
 |-  ( H e. ( R GrpHom S ) -> H e. ( R MndHom S ) )
36 8 34 35 3syl 
 |-  ( ph -> H e. ( R MndHom S ) )
37 36 adantr 
 |-  ( ( ph /\ k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } ) -> H e. ( R MndHom S ) )
38 eqid 
 |-  ( .r ` R ) = ( .r ` R )
39 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 } ) -> R e. Ring )
40 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 } ) -> F : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
41 breq1 
 |-  ( e = d -> ( e oR <_ k <-> d oR <_ k ) )
42 41 elrab 
 |-  ( 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 } /\ d oR <_ k ) )
43 42 biimpi 
 |-  ( 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 } /\ d oR <_ k ) )
44 43 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 } /\ d oR <_ k ) )
45 44 simpld 
 |-  ( ( ( 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 } )
46 40 45 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 } ) -> ( F ` d ) e. ( Base ` R ) )
47 19 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 ) )
48 simplr 
 |-  ( ( ( 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 e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
49 15 psrbagf 
 |-  ( d e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } -> d : I --> NN0 )
50 45 49 syl 
 |-  ( ( ( 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 : I --> NN0 )
51 44 simprd 
 |-  ( ( ( 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 oR <_ k )
52 15 psrbagcon 
 |-  ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } /\ d : I --> NN0 /\ d oR <_ k ) -> ( ( k oF - d ) e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } /\ ( k oF - d ) oR <_ k ) )
53 48 50 51 52 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 } ) -> ( ( k oF - d ) e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } /\ ( k oF - d ) oR <_ k ) )
54 53 simpld 
 |-  ( ( ( 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 } )
55 47 54 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 ) )
56 11 38 39 46 55 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 ) )
57 15 17 18 19 rhmmpllem1 
 |-  ( ( 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 ) )
58 11 22 24 29 33 37 56 57 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 ) ) ) ) ) ) )
59 8 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 ) )
60 eqid 
 |-  ( .r ` S ) = ( .r ` S )
61 11 38 60 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 ) ) ) ) )
62 59 46 55 61 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 ) ) ) ) )
63 40 45 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 ) ) )
64 47 54 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 ) ) ) )
65 63 64 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 ) ) ) ) )
66 62 65 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 ) ) ) )
67 66 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 ) ) ) ) )
68 67 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 ) ) ) ) ) )
69 58 68 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 ) ) ) ) ) )
70 69 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 ) ) ) ) ) ) )
71 21 70 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 ) ) ) ) ) ) )
72 1 3 38 5 15 9 10 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 ) ) ) ) ) ) )
73 72 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 ) ) ) ) ) ) ) )
74 1 2 3 4 7 36 9 mhmcompl 
 |-  ( ph -> ( H o. F ) e. C )
75 1 2 3 4 7 36 10 mhmcompl 
 |-  ( ph -> ( H o. G ) e. C )
76 2 4 60 6 15 74 75 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 ) ) ) ) ) ) )
77 71 73 76 3eqtr4d 
 |-  ( ph -> ( H o. ( F .x. G ) ) = ( ( H o. F ) .xb ( H o. G ) ) )