# Metamath Proof Explorer

## Theorem ismgmhm

Description: Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses ismgmhm.b 𝐵 = ( Base ‘ 𝑆 )
ismgmhm.c 𝐶 = ( Base ‘ 𝑇 )
ismgmhm.p + = ( +g𝑆 )
ismgmhm.q = ( +g𝑇 )
Assertion ismgmhm ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( 𝐹 : 𝐵𝐶 ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹𝑥 ) ( 𝐹𝑦 ) ) ) ) )

### Proof

Step Hyp Ref Expression
1 ismgmhm.b 𝐵 = ( Base ‘ 𝑆 )
2 ismgmhm.c 𝐶 = ( Base ‘ 𝑇 )
3 ismgmhm.p + = ( +g𝑆 )
4 ismgmhm.q = ( +g𝑇 )
5 mgmhmrcl ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
6 fveq2 ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = ( Base ‘ 𝑇 ) )
7 6 2 syl6eqr ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = 𝐶 )
8 fveq2 ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
9 8 1 syl6eqr ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = 𝐵 )
10 7 9 oveqan12rd ( ( 𝑠 = 𝑆𝑡 = 𝑇 ) → ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) = ( 𝐶m 𝐵 ) )
11 9 adantr ( ( 𝑠 = 𝑆𝑡 = 𝑇 ) → ( Base ‘ 𝑠 ) = 𝐵 )
12 fveq2 ( 𝑠 = 𝑆 → ( +g𝑠 ) = ( +g𝑆 ) )
13 12 3 syl6eqr ( 𝑠 = 𝑆 → ( +g𝑠 ) = + )
14 13 oveqd ( 𝑠 = 𝑆 → ( 𝑥 ( +g𝑠 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
15 14 fveq2d ( 𝑠 = 𝑆 → ( 𝑓 ‘ ( 𝑥 ( +g𝑠 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) )
16 fveq2 ( 𝑡 = 𝑇 → ( +g𝑡 ) = ( +g𝑇 ) )
17 16 4 syl6eqr ( 𝑡 = 𝑇 → ( +g𝑡 ) = )
18 17 oveqd ( 𝑡 = 𝑇 → ( ( 𝑓𝑥 ) ( +g𝑡 ) ( 𝑓𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) )
19 15 18 eqeqan12d ( ( 𝑠 = 𝑆𝑡 = 𝑇 ) → ( ( 𝑓 ‘ ( 𝑥 ( +g𝑠 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑡 ) ( 𝑓𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) ) )
20 11 19 raleqbidv ( ( 𝑠 = 𝑆𝑡 = 𝑇 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g𝑠 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑡 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑦𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) ) )
21 11 20 raleqbidv ( ( 𝑠 = 𝑆𝑡 = 𝑇 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g𝑠 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑡 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) ) )
22 10 21 rabeqbidv ( ( 𝑠 = 𝑆𝑡 = 𝑇 ) → { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g𝑠 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑡 ) ( 𝑓𝑦 ) ) } = { 𝑓 ∈ ( 𝐶m 𝐵 ) ∣ ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) } )
23 df-mgmhm MgmHom = ( 𝑠 ∈ Mgm , 𝑡 ∈ Mgm ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g𝑠 ) 𝑦 ) ) = ( ( 𝑓𝑥 ) ( +g𝑡 ) ( 𝑓𝑦 ) ) } )
24 ovex ( 𝐶m 𝐵 ) ∈ V
25 24 rabex { 𝑓 ∈ ( 𝐶m 𝐵 ) ∣ ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) } ∈ V
26 22 23 25 ovmpoa ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) → ( 𝑆 MgmHom 𝑇 ) = { 𝑓 ∈ ( 𝐶m 𝐵 ) ∣ ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) } )
27 26 eleq2d ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) → ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝐶m 𝐵 ) ∣ ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) } ) )
28 fveq1 ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
29 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝑥 ) = ( 𝐹𝑥 ) )
30 fveq1 ( 𝑓 = 𝐹 → ( 𝑓𝑦 ) = ( 𝐹𝑦 ) )
31 29 30 oveq12d ( 𝑓 = 𝐹 → ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) = ( ( 𝐹𝑥 ) ( 𝐹𝑦 ) ) )
32 28 31 eqeq12d ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹𝑥 ) ( 𝐹𝑦 ) ) ) )
33 32 2ralbidv ( 𝑓 = 𝐹 → ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹𝑥 ) ( 𝐹𝑦 ) ) ) )
34 33 elrab ( 𝐹 ∈ { 𝑓 ∈ ( 𝐶m 𝐵 ) ∣ ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) } ↔ ( 𝐹 ∈ ( 𝐶m 𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹𝑥 ) ( 𝐹𝑦 ) ) ) )
35 2 fvexi 𝐶 ∈ V
36 1 fvexi 𝐵 ∈ V
37 35 36 elmap ( 𝐹 ∈ ( 𝐶m 𝐵 ) ↔ 𝐹 : 𝐵𝐶 )
38 37 anbi1i ( ( 𝐹 ∈ ( 𝐶m 𝐵 ) ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹𝑥 ) ( 𝐹𝑦 ) ) ) ↔ ( 𝐹 : 𝐵𝐶 ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹𝑥 ) ( 𝐹𝑦 ) ) ) )
39 34 38 bitri ( 𝐹 ∈ { 𝑓 ∈ ( 𝐶m 𝐵 ) ∣ ∀ 𝑥𝐵𝑦𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓𝑥 ) ( 𝑓𝑦 ) ) } ↔ ( 𝐹 : 𝐵𝐶 ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹𝑥 ) ( 𝐹𝑦 ) ) ) )
40 27 39 syl6bb ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) → ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ ( 𝐹 : 𝐵𝐶 ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹𝑥 ) ( 𝐹𝑦 ) ) ) ) )
41 5 40 biadanii ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( 𝐹 : 𝐵𝐶 ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹𝑥 ) ( 𝐹𝑦 ) ) ) ) )