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 ffvelcdm ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐶 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 )
10 ffvelcdm ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐶 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑓 ‘ 𝑦 ) ∈ 𝐶 )
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 𝑀 ) )