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 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = 𝐶 )
8 fveq2 ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
9 8 1 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = 𝐵 )
10 7 9 oveqan12rd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) = ( 𝐶 ↑m 𝐵 ) )
11 9 adantr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( Base ‘ 𝑠 ) = 𝐵 )
12 fveq2 ⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = ( +g ‘ 𝑆 ) )
13 12 3 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = + )
14 13 oveqd ⊢ ( 𝑠 = 𝑆 → ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
15 14 fveq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) )
16 fveq2 ⊢ ( 𝑡 = 𝑇 → ( +g ‘ 𝑡 ) = ( +g ‘ 𝑇 ) )
17 16 4 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( +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 bitrdi ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) → ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ) )
41 5 40 biadanii ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ) )