Metamath Proof Explorer


Theorem rhmcomulpsr

Description: Show that the ring homomorphism in rhmpsr preserves multiplication. (Contributed by SN, 18-May-2025)

Ref Expression
Hypotheses rhmcomulpsr.p P=ImPwSerR
rhmcomulpsr.q Q=ImPwSerS
rhmcomulpsr.b B=BaseP
rhmcomulpsr.c C=BaseQ
rhmcomulpsr.1 ·˙=P
rhmcomulpsr.2 ˙=Q
rhmcomulpsr.h φHRRingHomS
rhmcomulpsr.f φFB
rhmcomulpsr.g φGB
Assertion rhmcomulpsr φHF·˙G=HF˙HG

Proof

Step Hyp Ref Expression
1 rhmcomulpsr.p P=ImPwSerR
2 rhmcomulpsr.q Q=ImPwSerS
3 rhmcomulpsr.b B=BaseP
4 rhmcomulpsr.c C=BaseQ
5 rhmcomulpsr.1 ·˙=P
6 rhmcomulpsr.2 ˙=Q
7 rhmcomulpsr.h φHRRingHomS
8 rhmcomulpsr.f φFB
9 rhmcomulpsr.g φGB
10 eqid BaseR=BaseR
11 eqid BaseS=BaseS
12 10 11 rhmf HRRingHomSH:BaseRBaseS
13 7 12 syl φH:BaseRBaseS
14 eqid f0I|f-1Fin=f0I|f-1Fin
15 rhmrcl1 HRRingHomSRRing
16 7 15 syl φRRing
17 1 10 14 3 8 psrelbas φF:f0I|f-1FinBaseR
18 1 10 14 3 9 psrelbas φG:f0I|f-1FinBaseR
19 14 16 17 18 rhmpsrlem2 φkf0I|f-1FinRdef0I|f-1Fin|efkFdRGkfdBaseR
20 13 19 cofmpt φHkf0I|f-1FinRdef0I|f-1Fin|efkFdRGkfd=kf0I|f-1FinHRdef0I|f-1Fin|efkFdRGkfd
21 eqid 0R=0R
22 16 ringcmnd φRCMnd
23 22 adantr φkf0I|f-1FinRCMnd
24 rhmrcl2 HRRingHomSSRing
25 7 24 syl φSRing
26 25 ringgrpd φSGrp
27 26 grpmndd φSMnd
28 27 adantr φkf0I|f-1FinSMnd
29 ovex 0IV
30 29 rabex f0I|f-1FinV
31 30 rabex ef0I|f-1Fin|efkV
32 31 a1i φkf0I|f-1Finef0I|f-1Fin|efkV
33 rhmghm HRRingHomSHRGrpHomS
34 ghmmhm HRGrpHomSHRMndHomS
35 7 33 34 3syl φHRMndHomS
36 35 adantr φkf0I|f-1FinHRMndHomS
37 eqid R=R
38 16 ad2antrr φkf0I|f-1Findef0I|f-1Fin|efkRRing
39 elrabi def0I|f-1Fin|efkdf0I|f-1Fin
40 17 ffvelcdmda φdf0I|f-1FinFdBaseR
41 39 40 sylan2 φdef0I|f-1Fin|efkFdBaseR
42 41 adantlr φkf0I|f-1Findef0I|f-1Fin|efkFdBaseR
43 18 ad2antrr φkf0I|f-1Findef0I|f-1Fin|efkG:f0I|f-1FinBaseR
44 eqid ef0I|f-1Fin|efk=ef0I|f-1Fin|efk
45 14 44 psrbagconcl kf0I|f-1Findef0I|f-1Fin|efkkfdef0I|f-1Fin|efk
46 45 adantll φkf0I|f-1Findef0I|f-1Fin|efkkfdef0I|f-1Fin|efk
47 elrabi kfdef0I|f-1Fin|efkkfdf0I|f-1Fin
48 46 47 syl φkf0I|f-1Findef0I|f-1Fin|efkkfdf0I|f-1Fin
49 43 48 ffvelcdmd φkf0I|f-1Findef0I|f-1Fin|efkGkfdBaseR
50 10 37 38 42 49 ringcld φkf0I|f-1Findef0I|f-1Fin|efkFdRGkfdBaseR
51 14 16 17 18 rhmpsrlem1 φkf0I|f-1FinfinSupp0Rdef0I|f-1Fin|efkFdRGkfd
52 10 21 23 28 32 36 50 51 gsummptmhm φkf0I|f-1FinSdef0I|f-1Fin|efkHFdRGkfd=HRdef0I|f-1Fin|efkFdRGkfd
53 7 ad2antrr φkf0I|f-1Findef0I|f-1Fin|efkHRRingHomS
54 eqid S=S
55 10 37 54 rhmmul HRRingHomSFdBaseRGkfdBaseRHFdRGkfd=HFdSHGkfd
56 53 42 49 55 syl3anc φkf0I|f-1Findef0I|f-1Fin|efkHFdRGkfd=HFdSHGkfd
57 17 ad2antrr φkf0I|f-1Findef0I|f-1Fin|efkF:f0I|f-1FinBaseR
58 39 adantl φkf0I|f-1Findef0I|f-1Fin|efkdf0I|f-1Fin
59 57 58 fvco3d φkf0I|f-1Findef0I|f-1Fin|efkHFd=HFd
60 43 48 fvco3d φkf0I|f-1Findef0I|f-1Fin|efkHGkfd=HGkfd
61 59 60 oveq12d φkf0I|f-1Findef0I|f-1Fin|efkHFdSHGkfd=HFdSHGkfd
62 56 61 eqtr4d φkf0I|f-1Findef0I|f-1Fin|efkHFdRGkfd=HFdSHGkfd
63 62 mpteq2dva φkf0I|f-1Findef0I|f-1Fin|efkHFdRGkfd=def0I|f-1Fin|efkHFdSHGkfd
64 63 oveq2d φkf0I|f-1FinSdef0I|f-1Fin|efkHFdRGkfd=Sdef0I|f-1Fin|efkHFdSHGkfd
65 52 64 eqtr3d φkf0I|f-1FinHRdef0I|f-1Fin|efkFdRGkfd=Sdef0I|f-1Fin|efkHFdSHGkfd
66 65 mpteq2dva φkf0I|f-1FinHRdef0I|f-1Fin|efkFdRGkfd=kf0I|f-1FinSdef0I|f-1Fin|efkHFdSHGkfd
67 20 66 eqtrd φHkf0I|f-1FinRdef0I|f-1Fin|efkFdRGkfd=kf0I|f-1FinSdef0I|f-1Fin|efkHFdSHGkfd
68 1 3 37 5 14 8 9 psrmulfval φF·˙G=kf0I|f-1FinRdef0I|f-1Fin|efkFdRGkfd
69 68 coeq2d φHF·˙G=Hkf0I|f-1FinRdef0I|f-1Fin|efkFdRGkfd
70 1 2 3 4 35 8 mhmcopsr φHFC
71 1 2 3 4 35 9 mhmcopsr φHGC
72 2 4 54 6 14 70 71 psrmulfval φHF˙HG=kf0I|f-1FinSdef0I|f-1Fin|efkHFdSHGkfd
73 67 69 72 3eqtr4d φHF·˙G=HF˙HG