Metamath Proof Explorer


Theorem mgmhmpropd

Description: Magma homomorphism depends only on the operation of structures. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses mgmhmpropd.a φB=BaseJ
mgmhmpropd.b φC=BaseK
mgmhmpropd.c φB=BaseL
mgmhmpropd.d φC=BaseM
mgmhmpropd.0 φB
mgmhmpropd.C φC
mgmhmpropd.e φxByBx+Jy=x+Ly
mgmhmpropd.f φxCyCx+Ky=x+My
Assertion mgmhmpropd φJMgmHomK=LMgmHomM

Proof

Step Hyp Ref Expression
1 mgmhmpropd.a φB=BaseJ
2 mgmhmpropd.b φC=BaseK
3 mgmhmpropd.c φB=BaseL
4 mgmhmpropd.d φC=BaseM
5 mgmhmpropd.0 φB
6 mgmhmpropd.C φC
7 mgmhmpropd.e φxByBx+Jy=x+Ly
8 mgmhmpropd.f φxCyCx+Ky=x+My
9 7 fveq2d φxByBfx+Jy=fx+Ly
10 9 adantlr φf:BCxByBfx+Jy=fx+Ly
11 ffvelcdm f:BCxBfxC
12 ffvelcdm f:BCyBfyC
13 11 12 anim12dan f:BCxByBfxCfyC
14 8 ralrimivva φxCyCx+Ky=x+My
15 oveq1 x=wx+Ky=w+Ky
16 oveq1 x=wx+My=w+My
17 15 16 eqeq12d x=wx+Ky=x+Myw+Ky=w+My
18 oveq2 y=zw+Ky=w+Kz
19 oveq2 y=zw+My=w+Mz
20 18 19 eqeq12d y=zw+Ky=w+Myw+Kz=w+Mz
21 17 20 cbvral2vw xCyCx+Ky=x+MywCzCw+Kz=w+Mz
22 14 21 sylib φwCzCw+Kz=w+Mz
23 oveq1 w=fxw+Kz=fx+Kz
24 oveq1 w=fxw+Mz=fx+Mz
25 23 24 eqeq12d w=fxw+Kz=w+Mzfx+Kz=fx+Mz
26 oveq2 z=fyfx+Kz=fx+Kfy
27 oveq2 z=fyfx+Mz=fx+Mfy
28 26 27 eqeq12d z=fyfx+Kz=fx+Mzfx+Kfy=fx+Mfy
29 25 28 rspc2va fxCfyCwCzCw+Kz=w+Mzfx+Kfy=fx+Mfy
30 13 22 29 syl2anr φf:BCxByBfx+Kfy=fx+Mfy
31 30 anassrs φf:BCxByBfx+Kfy=fx+Mfy
32 10 31 eqeq12d φf:BCxByBfx+Jy=fx+Kfyfx+Ly=fx+Mfy
33 32 2ralbidva φf:BCxByBfx+Jy=fx+KfyxByBfx+Ly=fx+Mfy
34 33 adantrl φJMgmKMgmf:BCxByBfx+Jy=fx+KfyxByBfx+Ly=fx+Mfy
35 raleq B=BaseJyBfx+Jy=fx+KfyyBaseJfx+Jy=fx+Kfy
36 35 raleqbi1dv B=BaseJxByBfx+Jy=fx+KfyxBaseJyBaseJfx+Jy=fx+Kfy
37 1 36 syl φxByBfx+Jy=fx+KfyxBaseJyBaseJfx+Jy=fx+Kfy
38 37 adantr φJMgmKMgmf:BCxByBfx+Jy=fx+KfyxBaseJyBaseJfx+Jy=fx+Kfy
39 raleq B=BaseLyBfx+Ly=fx+MfyyBaseLfx+Ly=fx+Mfy
40 39 raleqbi1dv B=BaseLxByBfx+Ly=fx+MfyxBaseLyBaseLfx+Ly=fx+Mfy
41 3 40 syl φxByBfx+Ly=fx+MfyxBaseLyBaseLfx+Ly=fx+Mfy
42 41 adantr φJMgmKMgmf:BCxByBfx+Ly=fx+MfyxBaseLyBaseLfx+Ly=fx+Mfy
43 34 38 42 3bitr3d φJMgmKMgmf:BCxBaseJyBaseJfx+Jy=fx+KfyxBaseLyBaseLfx+Ly=fx+Mfy
44 43 anassrs φJMgmKMgmf:BCxBaseJyBaseJfx+Jy=fx+KfyxBaseLyBaseLfx+Ly=fx+Mfy
45 44 pm5.32da φJMgmKMgmf:BCxBaseJyBaseJfx+Jy=fx+Kfyf:BCxBaseLyBaseLfx+Ly=fx+Mfy
46 1 2 feq23d φf:BCf:BaseJBaseK
47 46 adantr φJMgmKMgmf:BCf:BaseJBaseK
48 47 anbi1d φJMgmKMgmf:BCxBaseJyBaseJfx+Jy=fx+Kfyf:BaseJBaseKxBaseJyBaseJfx+Jy=fx+Kfy
49 3 4 feq23d φf:BCf:BaseLBaseM
50 49 adantr φJMgmKMgmf:BCf:BaseLBaseM
51 50 anbi1d φJMgmKMgmf:BCxBaseLyBaseLfx+Ly=fx+Mfyf:BaseLBaseMxBaseLyBaseLfx+Ly=fx+Mfy
52 45 48 51 3bitr3d φJMgmKMgmf:BaseJBaseKxBaseJyBaseJfx+Jy=fx+Kfyf:BaseLBaseMxBaseLyBaseLfx+Ly=fx+Mfy
53 52 pm5.32da φJMgmKMgmf:BaseJBaseKxBaseJyBaseJfx+Jy=fx+KfyJMgmKMgmf:BaseLBaseMxBaseLyBaseLfx+Ly=fx+Mfy
54 1 3 5 7 mgmpropd φJMgmLMgm
55 2 4 6 8 mgmpropd φKMgmMMgm
56 54 55 anbi12d φJMgmKMgmLMgmMMgm
57 56 anbi1d φJMgmKMgmf:BaseLBaseMxBaseLyBaseLfx+Ly=fx+MfyLMgmMMgmf:BaseLBaseMxBaseLyBaseLfx+Ly=fx+Mfy
58 53 57 bitrd φJMgmKMgmf:BaseJBaseKxBaseJyBaseJfx+Jy=fx+KfyLMgmMMgmf:BaseLBaseMxBaseLyBaseLfx+Ly=fx+Mfy
59 eqid BaseJ=BaseJ
60 eqid BaseK=BaseK
61 eqid +J=+J
62 eqid +K=+K
63 59 60 61 62 ismgmhm fJMgmHomKJMgmKMgmf:BaseJBaseKxBaseJyBaseJfx+Jy=fx+Kfy
64 eqid BaseL=BaseL
65 eqid BaseM=BaseM
66 eqid +L=+L
67 eqid +M=+M
68 64 65 66 67 ismgmhm fLMgmHomMLMgmMMgmf:BaseLBaseMxBaseLyBaseLfx+Ly=fx+Mfy
69 58 63 68 3bitr4g φfJMgmHomKfLMgmHomM
70 69 eqrdv φJMgmHomK=LMgmHomM