Metamath Proof Explorer


Theorem ghmpropd

Description: Group homomorphism depends only on the group attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses ghmpropd.a φB=BaseJ
ghmpropd.b φC=BaseK
ghmpropd.c φB=BaseL
ghmpropd.d φC=BaseM
ghmpropd.e φxByBx+Jy=x+Ly
ghmpropd.f φxCyCx+Ky=x+My
Assertion ghmpropd φJGrpHomK=LGrpHomM

Proof

Step Hyp Ref Expression
1 ghmpropd.a φB=BaseJ
2 ghmpropd.b φC=BaseK
3 ghmpropd.c φB=BaseL
4 ghmpropd.d φC=BaseM
5 ghmpropd.e φxByBx+Jy=x+Ly
6 ghmpropd.f φxCyCx+Ky=x+My
7 1 3 5 grppropd φJGrpLGrp
8 2 4 6 grppropd φKGrpMGrp
9 7 8 anbi12d φJGrpKGrpLGrpMGrp
10 1 2 3 4 5 6 mhmpropd φJMndHomK=LMndHomM
11 10 eleq2d φfJMndHomKfLMndHomM
12 9 11 anbi12d φJGrpKGrpfJMndHomKLGrpMGrpfLMndHomM
13 ghmgrp1 fJGrpHomKJGrp
14 ghmgrp2 fJGrpHomKKGrp
15 13 14 jca fJGrpHomKJGrpKGrp
16 ghmmhmb JGrpKGrpJGrpHomK=JMndHomK
17 16 eleq2d JGrpKGrpfJGrpHomKfJMndHomK
18 15 17 biadanii fJGrpHomKJGrpKGrpfJMndHomK
19 ghmgrp1 fLGrpHomMLGrp
20 ghmgrp2 fLGrpHomMMGrp
21 19 20 jca fLGrpHomMLGrpMGrp
22 ghmmhmb LGrpMGrpLGrpHomM=LMndHomM
23 22 eleq2d LGrpMGrpfLGrpHomMfLMndHomM
24 21 23 biadanii fLGrpHomMLGrpMGrpfLMndHomM
25 12 18 24 3bitr4g φfJGrpHomKfLGrpHomM
26 25 eqrdv φJGrpHomK=LGrpHomM