mhmpropd

Description: Monoid homomorphism depends only on the monoidal attributes of structures. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 7-Nov-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mhmpropd.a	$⊢ φ \to B = {Base}_{J}$
2		mhmpropd.b	$⊢ φ \to C = {Base}_{K}$
3		mhmpropd.c	$⊢ φ \to B = {Base}_{L}$
4		mhmpropd.d	$⊢ φ \to C = {Base}_{M}$
5		mhmpropd.e	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{J} y = x +_{L} y$
6		mhmpropd.f	$⊢ (φ \land (x \in C \land y \in C)) \to x +_{K} y = x +_{M} y$
7	5	fveq2d	$⊢ (φ \land (x \in B \land y \in B)) \to f (x +_{J} y) = f (x +_{L} y)$
8	7	adantlr	$⊢ ((φ \land f : B ⟶ C) \land (x \in B \land y \in B)) \to f (x +_{J} y) = f (x +_{L} y)$
9		ffvelcdm	$⊢ (f : B ⟶ C \land x \in B) \to f (x) \in C$
10		ffvelcdm	$⊢ (f : B ⟶ C \land y \in B) \to f (y) \in C$
11	9 10	anim12dan	$⊢ (f : B ⟶ C \land (x \in B \land y \in B)) \to (f (x) \in C \land f (y) \in C)$
12	6	ralrimivva	$⊢ φ \to \forall x \in C \forall y \in C x +_{K} y = x +_{M} y$
13		oveq1	$⊢ x = w \to x +_{K} y = w +_{K} y$
14		oveq1	$⊢ x = w \to x +_{M} y = w +_{M} y$
15	13 14	eqeq12d	$⊢ x = w \to (x +_{K} y = x +_{M} y \leftrightarrow w +_{K} y = w +_{M} y)$
16		oveq2	$⊢ y = z \to w +_{K} y = w +_{K} z$
17		oveq2	$⊢ y = z \to w +_{M} y = w +_{M} z$
18	16 17	eqeq12d	$⊢ y = z \to (w +_{K} y = w +_{M} y \leftrightarrow w +_{K} z = w +_{M} z)$
19	15 18	cbvral2vw	$⊢ \forall x \in C \forall y \in C x +_{K} y = x +_{M} y \leftrightarrow \forall w \in C \forall z \in C w +_{K} z = w +_{M} z$
20	12 19	sylib	$⊢ φ \to \forall w \in C \forall z \in C w +_{K} z = w +_{M} z$
21		oveq1	$⊢ w = f (x) \to w +_{K} z = f (x) +_{K} z$
22		oveq1	$⊢ w = f (x) \to w +_{M} z = f (x) +_{M} z$
23	21 22	eqeq12d	$⊢ w = f (x) \to (w +_{K} z = w +_{M} z \leftrightarrow f (x) +_{K} z = f (x) +_{M} z)$
24		oveq2	$⊢ z = f (y) \to f (x) +_{K} z = f (x) +_{K} f (y)$
25		oveq2	$⊢ z = f (y) \to f (x) +_{M} z = f (x) +_{M} f (y)$
26	24 25	eqeq12d	$⊢ z = f (y) \to (f (x) +_{K} z = f (x) +_{M} z \leftrightarrow f (x) +_{K} f (y) = f (x) +_{M} f (y))$
27	23 26	rspc2va	$⊢ ((f (x) \in C \land f (y) \in C) \land \forall w \in C \forall z \in C w +_{K} z = w +_{M} z) \to f (x) +_{K} f (y) = f (x) +_{M} f (y)$
28	11 20 27	syl2anr	$⊢ (φ \land (f : B ⟶ C \land (x \in B \land y \in B))) \to f (x) +_{K} f (y) = f (x) +_{M} f (y)$
29	28	anassrs	$⊢ ((φ \land f : B ⟶ C) \land (x \in B \land y \in B)) \to f (x) +_{K} f (y) = f (x) +_{M} f (y)$
30	8 29	eqeq12d	$⊢ ((φ \land f : B ⟶ C) \land (x \in B \land y \in B)) \to (f (x +_{J} y) = f (x) +_{K} f (y) \leftrightarrow f (x +_{L} y) = f (x) +_{M} f (y))$
31	30	2ralbidva	$⊢ (φ \land f : B ⟶ C) \to (\forall x \in B \forall y \in B f (x +_{J} y) = f (x) +_{K} f (y) \leftrightarrow \forall x \in B \forall y \in B f (x +_{L} y) = f (x) +_{M} f (y))$
32	31	adantrl	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to (\forall x \in B \forall y \in B f (x +_{J} y) = f (x) +_{K} f (y) \leftrightarrow \forall x \in B \forall y \in B f (x +_{L} y) = f (x) +_{M} f (y))$
33		raleq	$⊢ B = {Base}_{J} \to (\forall y \in B f (x +_{J} y) = f (x) +_{K} f (y) \leftrightarrow \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y))$
34	33	raleqbi1dv	$⊢ B = {Base}_{J} \to (\forall x \in B \forall y \in B f (x +_{J} y) = f (x) +_{K} f (y) \leftrightarrow \forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y))$
35	1 34	syl	$⊢ φ \to (\forall x \in B \forall y \in B f (x +_{J} y) = f (x) +_{K} f (y) \leftrightarrow \forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y))$
36	35	adantr	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to (\forall x \in B \forall y \in B f (x +_{J} y) = f (x) +_{K} f (y) \leftrightarrow \forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y))$
37		raleq	$⊢ B = {Base}_{L} \to (\forall y \in B f (x +_{L} y) = f (x) +_{M} f (y) \leftrightarrow \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y))$
38	37	raleqbi1dv	$⊢ B = {Base}_{L} \to (\forall x \in B \forall y \in B f (x +_{L} y) = f (x) +_{M} f (y) \leftrightarrow \forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y))$
39	3 38	syl	$⊢ φ \to (\forall x \in B \forall y \in B f (x +_{L} y) = f (x) +_{M} f (y) \leftrightarrow \forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y))$
40	39	adantr	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to (\forall x \in B \forall y \in B f (x +_{L} y) = f (x) +_{M} f (y) \leftrightarrow \forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y))$
41	32 36 40	3bitr3d	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to (\forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \leftrightarrow \forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y))$
42	1	adantr	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to B = {Base}_{J}$
43	3	adantr	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to B = {Base}_{L}$
44	5	adantlr	$⊢ ((φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \land (x \in B \land y \in B)) \to x +_{J} y = x +_{L} y$
45	42 43 44	grpidpropd	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to 0_{J} = 0_{L}$
46	45	fveq2d	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to f (0_{J}) = f (0_{L})$
47	2	adantr	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to C = {Base}_{K}$
48	4	adantr	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to C = {Base}_{M}$
49	6	adantlr	$⊢ ((φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \land (x \in C \land y \in C)) \to x +_{K} y = x +_{M} y$
50	47 48 49	grpidpropd	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to 0_{K} = 0_{M}$
51	46 50	eqeq12d	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to (f (0_{J}) = 0_{K} \leftrightarrow f (0_{L}) = 0_{M})$
52	41 51	anbi12d	$⊢ (φ \land ((J \in Mnd \land K \in Mnd) \land f : B ⟶ C)) \to ((\forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K}) \leftrightarrow (\forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M}))$
53	52	anassrs	$⊢ ((φ \land (J \in Mnd \land K \in Mnd)) \land f : B ⟶ C) \to ((\forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K}) \leftrightarrow (\forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M}))$
54	53	pm5.32da	$⊢ (φ \land (J \in Mnd \land K \in Mnd)) \to ((f : B ⟶ C \land (\forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K})) \leftrightarrow (f : B ⟶ C \land (\forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M})))$
55	1 2	feq23d	$⊢ φ \to (f : B ⟶ C \leftrightarrow f : {Base}_{J} ⟶ {Base}_{K})$
56	55	adantr	$⊢ (φ \land (J \in Mnd \land K \in Mnd)) \to (f : B ⟶ C \leftrightarrow f : {Base}_{J} ⟶ {Base}_{K})$
57	56	anbi1d	$⊢ (φ \land (J \in Mnd \land K \in Mnd)) \to ((f : B ⟶ C \land (\forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K})) \leftrightarrow (f : {Base}_{J} ⟶ {Base}_{K} \land (\forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K})))$
58	3 4	feq23d	$⊢ φ \to (f : B ⟶ C \leftrightarrow f : {Base}_{L} ⟶ {Base}_{M})$
59	58	adantr	$⊢ (φ \land (J \in Mnd \land K \in Mnd)) \to (f : B ⟶ C \leftrightarrow f : {Base}_{L} ⟶ {Base}_{M})$
60	59	anbi1d	$⊢ (φ \land (J \in Mnd \land K \in Mnd)) \to ((f : B ⟶ C \land (\forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M})) \leftrightarrow (f : {Base}_{L} ⟶ {Base}_{M} \land (\forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M})))$
61	54 57 60	3bitr3d	$⊢ (φ \land (J \in Mnd \land K \in Mnd)) \to ((f : {Base}_{J} ⟶ {Base}_{K} \land (\forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K})) \leftrightarrow (f : {Base}_{L} ⟶ {Base}_{M} \land (\forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M})))$
62		3anass	$⊢ (f : {Base}_{J} ⟶ {Base}_{K} \land \forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K}) \leftrightarrow (f : {Base}_{J} ⟶ {Base}_{K} \land (\forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K}))$
63		3anass	$⊢ (f : {Base}_{L} ⟶ {Base}_{M} \land \forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M}) \leftrightarrow (f : {Base}_{L} ⟶ {Base}_{M} \land (\forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M}))$
64	61 62 63	3bitr4g	$⊢ (φ \land (J \in Mnd \land K \in Mnd)) \to ((f : {Base}_{J} ⟶ {Base}_{K} \land \forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K}) \leftrightarrow (f : {Base}_{L} ⟶ {Base}_{M} \land \forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M}))$
65	64	pm5.32da	$⊢ φ \to (((J \in Mnd \land K \in Mnd) \land (f : {Base}_{J} ⟶ {Base}_{K} \land \forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K})) \leftrightarrow ((J \in Mnd \land K \in Mnd) \land (f : {Base}_{L} ⟶ {Base}_{M} \land \forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M})))$
66	1 3 5	mndpropd	$⊢ φ \to (J \in Mnd \leftrightarrow L \in Mnd)$
67	2 4 6	mndpropd	$⊢ φ \to (K \in Mnd \leftrightarrow M \in Mnd)$
68	66 67	anbi12d	$⊢ φ \to ((J \in Mnd \land K \in Mnd) \leftrightarrow (L \in Mnd \land M \in Mnd))$
69	68	anbi1d	$⊢ φ \to (((J \in Mnd \land K \in Mnd) \land (f : {Base}_{L} ⟶ {Base}_{M} \land \forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M})) \leftrightarrow ((L \in Mnd \land M \in Mnd) \land (f : {Base}_{L} ⟶ {Base}_{M} \land \forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M})))$
70	65 69	bitrd	$⊢ φ \to (((J \in Mnd \land K \in Mnd) \land (f : {Base}_{J} ⟶ {Base}_{K} \land \forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K})) \leftrightarrow ((L \in Mnd \land M \in Mnd) \land (f : {Base}_{L} ⟶ {Base}_{M} \land \forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M})))$
71		eqid	$⊢ {Base}_{J} = {Base}_{J}$
72		eqid	$⊢ {Base}_{K} = {Base}_{K}$
73		eqid	$⊢ +_{J} = +_{J}$
74		eqid	$⊢ +_{K} = +_{K}$
75		eqid	$⊢ 0_{J} = 0_{J}$
76		eqid	$⊢ 0_{K} = 0_{K}$
77	71 72 73 74 75 76	ismhm	$⊢ f \in (J MndHom K) \leftrightarrow ((J \in Mnd \land K \in Mnd) \land (f : {Base}_{J} ⟶ {Base}_{K} \land \forall x \in {Base}_{J} \forall y \in {Base}_{J} f (x +_{J} y) = f (x) +_{K} f (y) \land f (0_{J}) = 0_{K}))$
78		eqid	$⊢ {Base}_{L} = {Base}_{L}$
79		eqid	$⊢ {Base}_{M} = {Base}_{M}$
80		eqid	$⊢ +_{L} = +_{L}$
81		eqid	$⊢ +_{M} = +_{M}$
82		eqid	$⊢ 0_{L} = 0_{L}$
83		eqid	$⊢ 0_{M} = 0_{M}$
84	78 79 80 81 82 83	ismhm	$⊢ f \in (L MndHom M) \leftrightarrow ((L \in Mnd \land M \in Mnd) \land (f : {Base}_{L} ⟶ {Base}_{M} \land \forall x \in {Base}_{L} \forall y \in {Base}_{L} f (x +_{L} y) = f (x) +_{M} f (y) \land f (0_{L}) = 0_{M}))$
85	70 77 84	3bitr4g	$⊢ φ \to (f \in (J MndHom K) \leftrightarrow f \in (L MndHom M))$
86	85	eqrdv	$⊢ φ \to J MndHom K = L MndHom M$

Metamath Proof Explorer

Theorem mhmpropd

Proof