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 ( 𝜑𝐵 = ( Base ‘ 𝐽 ) )
ghmpropd.b ( 𝜑𝐶 = ( Base ‘ 𝐾 ) )
ghmpropd.c ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
ghmpropd.d ( 𝜑𝐶 = ( Base ‘ 𝑀 ) )
ghmpropd.e ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐽 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
ghmpropd.f ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) )
Assertion ghmpropd ( 𝜑 → ( 𝐽 GrpHom 𝐾 ) = ( 𝐿 GrpHom 𝑀 ) )

Proof

Step Hyp Ref Expression
1 ghmpropd.a ( 𝜑𝐵 = ( Base ‘ 𝐽 ) )
2 ghmpropd.b ( 𝜑𝐶 = ( Base ‘ 𝐾 ) )
3 ghmpropd.c ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
4 ghmpropd.d ( 𝜑𝐶 = ( Base ‘ 𝑀 ) )
5 ghmpropd.e ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐽 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
6 ghmpropd.f ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) )
7 1 3 5 grppropd ( 𝜑 → ( 𝐽 ∈ Grp ↔ 𝐿 ∈ Grp ) )
8 2 4 6 grppropd ( 𝜑 → ( 𝐾 ∈ Grp ↔ 𝑀 ∈ Grp ) )
9 7 8 anbi12d ( 𝜑 → ( ( 𝐽 ∈ Grp ∧ 𝐾 ∈ Grp ) ↔ ( 𝐿 ∈ Grp ∧ 𝑀 ∈ Grp ) ) )
10 1 2 3 4 5 6 mhmpropd ( 𝜑 → ( 𝐽 MndHom 𝐾 ) = ( 𝐿 MndHom 𝑀 ) )
11 10 eleq2d ( 𝜑 → ( 𝑓 ∈ ( 𝐽 MndHom 𝐾 ) ↔ 𝑓 ∈ ( 𝐿 MndHom 𝑀 ) ) )
12 9 11 anbi12d ( 𝜑 → ( ( ( 𝐽 ∈ Grp ∧ 𝐾 ∈ Grp ) ∧ 𝑓 ∈ ( 𝐽 MndHom 𝐾 ) ) ↔ ( ( 𝐿 ∈ Grp ∧ 𝑀 ∈ Grp ) ∧ 𝑓 ∈ ( 𝐿 MndHom 𝑀 ) ) ) )
13 ghmgrp1 ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) → 𝐽 ∈ Grp )
14 ghmgrp2 ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) → 𝐾 ∈ Grp )
15 13 14 jca ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) → ( 𝐽 ∈ Grp ∧ 𝐾 ∈ Grp ) )
16 ghmmhmb ( ( 𝐽 ∈ Grp ∧ 𝐾 ∈ Grp ) → ( 𝐽 GrpHom 𝐾 ) = ( 𝐽 MndHom 𝐾 ) )
17 16 eleq2d ( ( 𝐽 ∈ Grp ∧ 𝐾 ∈ Grp ) → ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ↔ 𝑓 ∈ ( 𝐽 MndHom 𝐾 ) ) )
18 15 17 biadanii ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ↔ ( ( 𝐽 ∈ Grp ∧ 𝐾 ∈ Grp ) ∧ 𝑓 ∈ ( 𝐽 MndHom 𝐾 ) ) )
19 ghmgrp1 ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) → 𝐿 ∈ Grp )
20 ghmgrp2 ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) → 𝑀 ∈ Grp )
21 19 20 jca ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) → ( 𝐿 ∈ Grp ∧ 𝑀 ∈ Grp ) )
22 ghmmhmb ( ( 𝐿 ∈ Grp ∧ 𝑀 ∈ Grp ) → ( 𝐿 GrpHom 𝑀 ) = ( 𝐿 MndHom 𝑀 ) )
23 22 eleq2d ( ( 𝐿 ∈ Grp ∧ 𝑀 ∈ Grp ) → ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ↔ 𝑓 ∈ ( 𝐿 MndHom 𝑀 ) ) )
24 21 23 biadanii ( 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ↔ ( ( 𝐿 ∈ Grp ∧ 𝑀 ∈ Grp ) ∧ 𝑓 ∈ ( 𝐿 MndHom 𝑀 ) ) )
25 12 18 24 3bitr4g ( 𝜑 → ( 𝑓 ∈ ( 𝐽 GrpHom 𝐾 ) ↔ 𝑓 ∈ ( 𝐿 GrpHom 𝑀 ) ) )
26 25 eqrdv ( 𝜑 → ( 𝐽 GrpHom 𝐾 ) = ( 𝐿 GrpHom 𝑀 ) )