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 ) ) )