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 · ˙ = P
rhmcomulmpl.2 ˙ = Q
rhmcomulmpl.h φ H R RingHom S
rhmcomulmpl.f φ F B
rhmcomulmpl.g φ G B
Assertion rhmcomulmpl φ H F · ˙ G = H F ˙ H 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 · ˙ = P
6 rhmcomulmpl.2 ˙ = Q
7 rhmcomulmpl.h φ H R RingHom S
8 rhmcomulmpl.f φ F B
9 rhmcomulmpl.g φ G B
10 eqid Base R = Base R
11 eqid Base S = Base S
12 10 11 rhmf H R RingHom S H : Base R Base S
13 7 12 syl φ H : Base R Base S
14 eqid f 0 I | f -1 Fin = f 0 I | f -1 Fin
15 rhmrcl1 H R RingHom S R Ring
16 7 15 syl φ R Ring
17 1 10 3 14 8 mplelf φ F : f 0 I | f -1 Fin Base R
18 1 10 3 14 9 mplelf φ G : f 0 I | f -1 Fin Base R
19 14 16 17 18 rhmpsrlem2 φ k f 0 I | f -1 Fin R d e f 0 I | f -1 Fin | e f k F d R G k f d Base R
20 13 19 cofmpt φ H k f 0 I | f -1 Fin R d e f 0 I | f -1 Fin | e f k F d R G k f d = k f 0 I | f -1 Fin H R d e f 0 I | f -1 Fin | e f k F d R G k f d
21 eqid 0 R = 0 R
22 16 ringcmnd φ R CMnd
23 22 adantr φ k f 0 I | f -1 Fin R CMnd
24 rhmrcl2 H R RingHom S S Ring
25 7 24 syl φ S Ring
26 25 ringgrpd φ S Grp
27 26 grpmndd φ S Mnd
28 27 adantr φ k f 0 I | f -1 Fin S Mnd
29 ovex 0 I V
30 29 rabex f 0 I | f -1 Fin V
31 30 rabex e f 0 I | f -1 Fin | e f k V
32 31 a1i φ k f 0 I | f -1 Fin e f 0 I | f -1 Fin | e f k V
33 rhmghm H R RingHom S H R GrpHom S
34 ghmmhm H R GrpHom S H R MndHom S
35 7 33 34 3syl φ H R MndHom S
36 35 adantr φ k f 0 I | f -1 Fin H R MndHom S
37 eqid R = R
38 16 ad2antrr φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k R Ring
39 elrabi d e f 0 I | f -1 Fin | e f k d f 0 I | f -1 Fin
40 17 ffvelcdmda φ d f 0 I | f -1 Fin F d Base R
41 39 40 sylan2 φ d e f 0 I | f -1 Fin | e f k F d Base R
42 41 adantlr φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k F d Base R
43 18 ad2antrr φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k G : f 0 I | f -1 Fin Base R
44 eqid e f 0 I | f -1 Fin | e f k = e f 0 I | f -1 Fin | e f k
45 14 44 psrbagconcl k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k k f d e f 0 I | f -1 Fin | e f k
46 elrabi k f d e f 0 I | f -1 Fin | e f k k f d f 0 I | f -1 Fin
47 45 46 syl k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k k f d f 0 I | f -1 Fin
48 47 adantll φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k k f d f 0 I | f -1 Fin
49 43 48 ffvelcdmd φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k G k f d Base R
50 10 37 38 42 49 ringcld φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k F d R G k f d Base R
51 14 16 17 18 rhmpsrlem1 φ k f 0 I | f -1 Fin finSupp 0 R d e f 0 I | f -1 Fin | e f k F d R G k f d
52 10 21 23 28 32 36 50 51 gsummptmhm φ k f 0 I | f -1 Fin S d e f 0 I | f -1 Fin | e f k H F d R G k f d = H R d e f 0 I | f -1 Fin | e f k F d R G k f d
53 7 ad2antrr φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k H R RingHom S
54 eqid S = S
55 10 37 54 rhmmul H R RingHom S F d Base R G k f d Base R H F d R G k f d = H F d S H G k f d
56 53 42 49 55 syl3anc φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k H F d R G k f d = H F d S H G k f d
57 17 ad2antrr φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k F : f 0 I | f -1 Fin Base R
58 39 adantl φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k d f 0 I | f -1 Fin
59 57 58 fvco3d φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k H F d = H F d
60 43 48 fvco3d φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k H G k f d = H G k f d
61 59 60 oveq12d φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k H F d S H G k f d = H F d S H G k f d
62 56 61 eqtr4d φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k H F d R G k f d = H F d S H G k f d
63 62 mpteq2dva φ k f 0 I | f -1 Fin d e f 0 I | f -1 Fin | e f k H F d R G k f d = d e f 0 I | f -1 Fin | e f k H F d S H G k f d
64 63 oveq2d φ k f 0 I | f -1 Fin S d e f 0 I | f -1 Fin | e f k H F d R G k f d = S d e f 0 I | f -1 Fin | e f k H F d S H G k f d
65 52 64 eqtr3d φ k f 0 I | f -1 Fin H R d e f 0 I | f -1 Fin | e f k F d R G k f d = S d e f 0 I | f -1 Fin | e f k H F d S H G k f d
66 65 mpteq2dva φ k f 0 I | f -1 Fin H R d e f 0 I | f -1 Fin | e f k F d R G k f d = k f 0 I | f -1 Fin S d e f 0 I | f -1 Fin | e f k H F d S H G k f d
67 20 66 eqtrd φ H k f 0 I | f -1 Fin R d e f 0 I | f -1 Fin | e f k F d R G k f d = k f 0 I | f -1 Fin S d e f 0 I | f -1 Fin | e f k H F d S H G k f d
68 1 3 37 5 14 8 9 mplmul φ F · ˙ G = k f 0 I | f -1 Fin R d e f 0 I | f -1 Fin | e f k F d R G k f d
69 68 coeq2d φ H F · ˙ G = H k f 0 I | f -1 Fin R d e f 0 I | f -1 Fin | e f k F d R G k f d
70 1 2 3 4 35 8 mhmcompl φ H F C
71 1 2 3 4 35 9 mhmcompl φ H G C
72 2 4 54 6 14 70 71 mplmul φ H F ˙ H G = k f 0 I | f -1 Fin S d e f 0 I | f -1 Fin | e f k H F d S H G k f d
73 67 69 72 3eqtr4d φ H F · ˙ G = H F ˙ H G