Metamath Proof Explorer

Theorem mgmhmpropd

Description: Magma homomorphism depends only on the operation of structures. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses mgmhmpropd.a ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐽 ) )
mgmhmpropd.b ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝐾 ) )
mgmhmpropd.c ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
mgmhmpropd.d ⊢ ( 𝜑 → 𝐶 = ( Base ‘ 𝑀 ) )
mgmhmpropd.0 ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
mgmhmpropd.C ⊢ ( 𝜑 → 𝐶 ≠ ∅ )
mgmhmpropd.e ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐽 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
mgmhmpropd.f ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) )
Assertion mgmhmpropd ( 𝜑 → ( 𝐽 MgmHom 𝐾 ) = ( 𝐿 MgmHom 𝑀 ) )

Proof

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