ghmpropd

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

	Ref	Expression
Hypotheses	ghmpropd.a	$⊢ φ \to B = {Base}_{J}$
	ghmpropd.b	$⊢ φ \to C = {Base}_{K}$
	ghmpropd.c	$⊢ φ \to B = {Base}_{L}$
	ghmpropd.d	$⊢ φ \to C = {Base}_{M}$
	ghmpropd.e	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{J} y = x +_{L} y$
	ghmpropd.f	$⊢ (φ \land (x \in C \land y \in C)) \to x +_{K} y = x +_{M} y$
Assertion	ghmpropd	$⊢ φ \to J GrpHom K = L GrpHom M$

Proof

Step	Hyp	Ref	Expression
1		ghmpropd.a	$⊢ φ \to B = {Base}_{J}$
2		ghmpropd.b	$⊢ φ \to C = {Base}_{K}$
3		ghmpropd.c	$⊢ φ \to B = {Base}_{L}$
4		ghmpropd.d	$⊢ φ \to C = {Base}_{M}$
5		ghmpropd.e	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{J} y = x +_{L} y$
6		ghmpropd.f	$⊢ (φ \land (x \in C \land y \in C)) \to x +_{K} y = x +_{M} y$
7	1 3 5	grppropd	$⊢ φ \to (J \in Grp \leftrightarrow L \in Grp)$
8	2 4 6	grppropd	$⊢ φ \to (K \in Grp \leftrightarrow M \in Grp)$
9	7 8	anbi12d	$⊢ φ \to ((J \in Grp \land K \in Grp) \leftrightarrow (L \in Grp \land M \in Grp))$
10	1 2 3 4 5 6	mhmpropd	$⊢ φ \to J MndHom K = L MndHom M$
11	10	eleq2d	$⊢ φ \to (f \in (J MndHom K) \leftrightarrow f \in (L MndHom M))$
12	9 11	anbi12d	$⊢ φ \to (((J \in Grp \land K \in Grp) \land f \in (J MndHom K)) \leftrightarrow ((L \in Grp \land M \in Grp) \land f \in (L MndHom M)))$
13		ghmgrp1	$⊢ f \in (J GrpHom K) \to J \in Grp$
14		ghmgrp2	$⊢ f \in (J GrpHom K) \to K \in Grp$
15	13 14	jca	$⊢ f \in (J GrpHom K) \to (J \in Grp \land K \in Grp)$
16		ghmmhmb	$⊢ (J \in Grp \land K \in Grp) \to J GrpHom K = J MndHom K$
17	16	eleq2d	$⊢ (J \in Grp \land K \in Grp) \to (f \in (J GrpHom K) \leftrightarrow f \in (J MndHom K))$
18	15 17	biadanii	$⊢ f \in (J GrpHom K) \leftrightarrow ((J \in Grp \land K \in Grp) \land f \in (J MndHom K))$
19		ghmgrp1	$⊢ f \in (L GrpHom M) \to L \in Grp$
20		ghmgrp2	$⊢ f \in (L GrpHom M) \to M \in Grp$
21	19 20	jca	$⊢ f \in (L GrpHom M) \to (L \in Grp \land M \in Grp)$
22		ghmmhmb	$⊢ (L \in Grp \land M \in Grp) \to L GrpHom M = L MndHom M$
23	22	eleq2d	$⊢ (L \in Grp \land M \in Grp) \to (f \in (L GrpHom M) \leftrightarrow f \in (L MndHom M))$
24	21 23	biadanii	$⊢ f \in (L GrpHom M) \leftrightarrow ((L \in Grp \land M \in Grp) \land f \in (L MndHom M))$
25	12 18 24	3bitr4g	$⊢ φ \to (f \in (J GrpHom K) \leftrightarrow f \in (L GrpHom M))$
26	25	eqrdv	$⊢ φ \to J GrpHom K = L GrpHom M$

Metamath Proof Explorer

Theorem ghmpropd

Proof