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 𝑀 ) )