Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 mhmpropd.a ( 𝜑𝐵 = ( Base ‘ 𝐽 ) )
2 mhmpropd.b ( 𝜑𝐶 = ( Base ‘ 𝐾 ) )
3 mhmpropd.c ( 𝜑𝐵 = ( Base ‘ 𝐿 ) )
4 mhmpropd.d ( 𝜑𝐶 = ( Base ‘ 𝑀 ) )
5 mhmpropd.e ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐽 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
6 mhmpropd.f ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) )
7 5 fveq2d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) )
8 7 adantlr ( ( ( 𝜑𝑓 : 𝐵𝐶 ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) )
9 ffvelrn ( ( 𝑓 : 𝐵𝐶𝑥𝐵 ) → ( 𝑓𝑥 ) ∈ 𝐶 )
10 ffvelrn ( ( 𝑓 : 𝐵𝐶𝑦𝐵 ) → ( 𝑓𝑦 ) ∈ 𝐶 )
11 9 10 anim12dan ( ( 𝑓 : 𝐵𝐶 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑓𝑥 ) ∈ 𝐶 ∧ ( 𝑓𝑦 ) ∈ 𝐶 ) )
12 6 ralrimivva ( 𝜑 → ∀ 𝑥𝐶𝑦𝐶 ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) )
13 oveq1 ( 𝑥 = 𝑤 → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑤 ( +g𝐾 ) 𝑦 ) )
14 oveq1 ( 𝑥 = 𝑤 → ( 𝑥 ( +g𝑀 ) 𝑦 ) = ( 𝑤 ( +g𝑀 ) 𝑦 ) )
15 13 14 eqeq12d ( 𝑥 = 𝑤 → ( ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) ↔ ( 𝑤 ( +g𝐾 ) 𝑦 ) = ( 𝑤 ( +g𝑀 ) 𝑦 ) ) )
16 oveq2 ( 𝑦 = 𝑧 → ( 𝑤 ( +g𝐾 ) 𝑦 ) = ( 𝑤 ( +g𝐾 ) 𝑧 ) )
17 oveq2 ( 𝑦 = 𝑧 → ( 𝑤 ( +g𝑀 ) 𝑦 ) = ( 𝑤 ( +g𝑀 ) 𝑧 ) )
18 16 17 eqeq12d ( 𝑦 = 𝑧 → ( ( 𝑤 ( +g𝐾 ) 𝑦 ) = ( 𝑤 ( +g𝑀 ) 𝑦 ) ↔ ( 𝑤 ( +g𝐾 ) 𝑧 ) = ( 𝑤 ( +g𝑀 ) 𝑧 ) ) )
19 15 18 cbvral2vw ( ∀ 𝑥𝐶𝑦𝐶 ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) ↔ ∀ 𝑤𝐶𝑧𝐶 ( 𝑤 ( +g𝐾 ) 𝑧 ) = ( 𝑤 ( +g𝑀 ) 𝑧 ) )
20 12 19 sylib ( 𝜑 → ∀ 𝑤𝐶𝑧𝐶 ( 𝑤 ( +g𝐾 ) 𝑧 ) = ( 𝑤 ( +g𝑀 ) 𝑧 ) )
21 oveq1 ( 𝑤 = ( 𝑓𝑥 ) → ( 𝑤 ( +g𝐾 ) 𝑧 ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) 𝑧 ) )
22 oveq1 ( 𝑤 = ( 𝑓𝑥 ) → ( 𝑤 ( +g𝑀 ) 𝑧 ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) 𝑧 ) )
23 21 22 eqeq12d ( 𝑤 = ( 𝑓𝑥 ) → ( ( 𝑤 ( +g𝐾 ) 𝑧 ) = ( 𝑤 ( +g𝑀 ) 𝑧 ) ↔ ( ( 𝑓𝑥 ) ( +g𝐾 ) 𝑧 ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) 𝑧 ) ) )
24 oveq2 ( 𝑧 = ( 𝑓𝑦 ) → ( ( 𝑓𝑥 ) ( +g𝐾 ) 𝑧 ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) )
25 oveq2 ( 𝑧 = ( 𝑓𝑦 ) → ( ( 𝑓𝑥 ) ( +g𝑀 ) 𝑧 ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) )
26 24 25 eqeq12d ( 𝑧 = ( 𝑓𝑦 ) → ( ( ( 𝑓𝑥 ) ( +g𝐾 ) 𝑧 ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) 𝑧 ) ↔ ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ) )
27 23 26 rspc2va ( ( ( ( 𝑓𝑥 ) ∈ 𝐶 ∧ ( 𝑓𝑦 ) ∈ 𝐶 ) ∧ ∀ 𝑤𝐶𝑧𝐶 ( 𝑤 ( +g𝐾 ) 𝑧 ) = ( 𝑤 ( +g𝑀 ) 𝑧 ) ) → ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) )
28 11 20 27 syl2anr ( ( 𝜑 ∧ ( 𝑓 : 𝐵𝐶 ∧ ( 𝑥𝐵𝑦𝐵 ) ) ) → ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) )
29 28 anassrs ( ( ( 𝜑𝑓 : 𝐵𝐶 ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) )
30 8 29 eqeq12d ( ( ( 𝜑𝑓 : 𝐵𝐶 ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ) )
31 30 2ralbidva ( ( 𝜑𝑓 : 𝐵𝐶 ) → ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ) )
32 31 adantrl ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ) )
33 raleq ( 𝐵 = ( Base ‘ 𝐽 ) → ( ∀ 𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ) )
34 33 raleqbi1dv ( 𝐵 = ( Base ‘ 𝐽 ) → ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ) )
35 1 34 syl ( 𝜑 → ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ) )
36 35 adantr ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ) )
37 raleq ( 𝐵 = ( Base ‘ 𝐿 ) → ( ∀ 𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ) )
38 37 raleqbi1dv ( 𝐵 = ( Base ‘ 𝐿 ) → ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ) )
39 3 38 syl ( 𝜑 → ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ) )
40 39 adantr ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ) )
41 32 36 40 3bitr3d ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ) )
42 1 adantr ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → 𝐵 = ( Base ‘ 𝐽 ) )
43 3 adantr ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → 𝐵 = ( Base ‘ 𝐿 ) )
44 5 adantlr ( ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐽 ) 𝑦 ) = ( 𝑥 ( +g𝐿 ) 𝑦 ) )
45 42 43 44 grpidpropd ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → ( 0g𝐽 ) = ( 0g𝐿 ) )
46 45 fveq2d ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 𝑓 ‘ ( 0g𝐿 ) ) )
47 2 adantr ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → 𝐶 = ( Base ‘ 𝐾 ) )
48 4 adantr ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → 𝐶 = ( Base ‘ 𝑀 ) )
49 6 adantlr ( ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 ( +g𝐾 ) 𝑦 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) )
50 47 48 49 grpidpropd ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → ( 0g𝐾 ) = ( 0g𝑀 ) )
51 46 50 eqeq12d ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → ( ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ↔ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) )
52 41 51 anbi12d ( ( 𝜑 ∧ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ 𝑓 : 𝐵𝐶 ) ) → ( ( ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ↔ ( ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) )
53 52 anassrs ( ( ( 𝜑 ∧ ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ) ∧ 𝑓 : 𝐵𝐶 ) → ( ( ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ↔ ( ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) )
54 53 pm5.32da ( ( 𝜑 ∧ ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ) → ( ( 𝑓 : 𝐵𝐶 ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ) ↔ ( 𝑓 : 𝐵𝐶 ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) ) )
55 1 2 feq23d ( 𝜑 → ( 𝑓 : 𝐵𝐶𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) ) )
56 55 adantr ( ( 𝜑 ∧ ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ) → ( 𝑓 : 𝐵𝐶𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) ) )
57 56 anbi1d ( ( 𝜑 ∧ ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ) → ( ( 𝑓 : 𝐵𝐶 ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ) ) )
58 3 4 feq23d ( 𝜑 → ( 𝑓 : 𝐵𝐶𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ) )
59 58 adantr ( ( 𝜑 ∧ ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ) → ( 𝑓 : 𝐵𝐶𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ) )
60 59 anbi1d ( ( 𝜑 ∧ ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ) → ( ( 𝑓 : 𝐵𝐶 ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) ) )
61 54 57 60 3bitr3d ( ( 𝜑 ∧ ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ) → ( ( 𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) ) )
62 3anass ( ( 𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ↔ ( 𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ) )
63 3anass ( ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ↔ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) )
64 61 62 63 3bitr4g ( ( 𝜑 ∧ ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ) → ( ( 𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ↔ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) )
65 64 pm5.32da ( 𝜑 → ( ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ) ↔ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) ) )
66 1 3 5 mndpropd ( 𝜑 → ( 𝐽 ∈ Mnd ↔ 𝐿 ∈ Mnd ) )
67 2 4 6 mndpropd ( 𝜑 → ( 𝐾 ∈ Mnd ↔ 𝑀 ∈ Mnd ) )
68 66 67 anbi12d ( 𝜑 → ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ↔ ( 𝐿 ∈ Mnd ∧ 𝑀 ∈ Mnd ) ) )
69 68 anbi1d ( 𝜑 → ( ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) ↔ ( ( 𝐿 ∈ Mnd ∧ 𝑀 ∈ Mnd ) ∧ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) ) )
70 65 69 bitrd ( 𝜑 → ( ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ) ↔ ( ( 𝐿 ∈ Mnd ∧ 𝑀 ∈ Mnd ) ∧ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) ) )
71 eqid ( Base ‘ 𝐽 ) = ( Base ‘ 𝐽 )
72 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
73 eqid ( +g𝐽 ) = ( +g𝐽 )
74 eqid ( +g𝐾 ) = ( +g𝐾 )
75 eqid ( 0g𝐽 ) = ( 0g𝐽 )
76 eqid ( 0g𝐾 ) = ( 0g𝐾 )
77 71 72 73 74 75 76 ismhm ( 𝑓 ∈ ( 𝐽 MndHom 𝐾 ) ↔ ( ( 𝐽 ∈ Mnd ∧ 𝐾 ∈ Mnd ) ∧ ( 𝑓 : ( Base ‘ 𝐽 ) ⟶ ( Base ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐽 ) ∀ 𝑦 ∈ ( Base ‘ 𝐽 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐽 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝐾 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐽 ) ) = ( 0g𝐾 ) ) ) )
78 eqid ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
79 eqid ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
80 eqid ( +g𝐿 ) = ( +g𝐿 )
81 eqid ( +g𝑀 ) = ( +g𝑀 )
82 eqid ( 0g𝐿 ) = ( 0g𝐿 )
83 eqid ( 0g𝑀 ) = ( 0g𝑀 )
84 78 79 80 81 82 83 ismhm ( 𝑓 ∈ ( 𝐿 MndHom 𝑀 ) ↔ ( ( 𝐿 ∈ Mnd ∧ 𝑀 ∈ Mnd ) ∧ ( 𝑓 : ( Base ‘ 𝐿 ) ⟶ ( Base ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐿 ) ∀ 𝑦 ∈ ( Base ‘ 𝐿 ) ( 𝑓 ‘ ( 𝑥 ( +g𝐿 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑀 ) ( 𝑓𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g𝐿 ) ) = ( 0g𝑀 ) ) ) )
85 70 77 84 3bitr4g ( 𝜑 → ( 𝑓 ∈ ( 𝐽 MndHom 𝐾 ) ↔ 𝑓 ∈ ( 𝐿 MndHom 𝑀 ) ) )
86 85 eqrdv ( 𝜑 → ( 𝐽 MndHom 𝐾 ) = ( 𝐿 MndHom 𝑀 ) )