Metamath Proof Explorer

Theorem ismhm

Description: Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypotheses ismhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
ismhm.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
ismhm.p ⊢ + = ( +g ‘ 𝑆 )
ismhm.q ⊢ ⨣ = ( +g ‘ 𝑇 )
ismhm.z ⊢ 0 = ( 0g ‘ 𝑆 )
ismhm.y ⊢ 𝑌 = ( 0g ‘ 𝑇 )
Assertion ismhm ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 ismhm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 ismhm.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
3 ismhm.p ⊢ + = ( +g ‘ 𝑆 )
4 ismhm.q ⊢ ⨣ = ( +g ‘ 𝑇 )
5 ismhm.z ⊢ 0 = ( 0g ‘ 𝑆 )
6 ismhm.y ⊢ 𝑌 = ( 0g ‘ 𝑇 )
7 df-mhm ⊢ MndHom = ( 𝑠 ∈ Mnd , 𝑡 ∈ Mnd ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 0g ‘ 𝑡 ) ) } )
8 7 elmpocl ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) )
9 fveq2 ⊢ ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = ( Base ‘ 𝑇 ) )
10 9 2 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = 𝐶 )
11 fveq2 ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
12 11 1 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = 𝐵 )
13 10 12 oveqan12rd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) = ( 𝐶 ↑m 𝐵 ) )
14 12 adantr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( Base ‘ 𝑠 ) = 𝐵 )
15 fveq2 ⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = ( +g ‘ 𝑆 ) )
16 15 3 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = + )
17 16 oveqd ⊢ ( 𝑠 = 𝑆 → ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
18 17 fveq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) )
19 fveq2 ⊢ ( 𝑡 = 𝑇 → ( +g ‘ 𝑡 ) = ( +g ‘ 𝑇 ) )
20 19 4 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( +g ‘ 𝑡 ) = ⨣ )
21 20 oveqd ⊢ ( 𝑡 = 𝑇 → ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) )
22 18 21 eqeqan12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
23 14 22 raleqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
24 14 23 raleqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ) )
25 fveq2 ⊢ ( 𝑠 = 𝑆 → ( 0g ‘ 𝑠 ) = ( 0g ‘ 𝑆 ) )
26 25 5 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( 0g ‘ 𝑠 ) = 0 )
27 26 fveq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 𝑓 ‘ 0 ) )
28 fveq2 ⊢ ( 𝑡 = 𝑇 → ( 0g ‘ 𝑡 ) = ( 0g ‘ 𝑇 ) )
29 28 6 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( 0g ‘ 𝑡 ) = 𝑌 )
30 27 29 eqeqan12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 0g ‘ 𝑡 ) ↔ ( 𝑓 ‘ 0 ) = 𝑌 ) )
31 24 30 anbi12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 0g ‘ 𝑡 ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑌 ) ) )
32 13 31 rabeqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 0g ‘ 𝑡 ) ) } = { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑌 ) } )
33 ovex ⊢ ( 𝐶 ↑m 𝐵 ) ∈ V
34 33 rabex ⊢ { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑌 ) } ∈ V
35 32 7 34 ovmpoa ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) → ( 𝑆 MndHom 𝑇 ) = { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑌 ) } )
36 35 eleq2d ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) → ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑌 ) } ) )
37 2 fvexi ⊢ 𝐶 ∈ V
38 1 fvexi ⊢ 𝐵 ∈ V
39 37 38 elmap ⊢ ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ↔ 𝐹 : 𝐵 ⟶ 𝐶 )
40 39 anbi1i ⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )
41 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) )
42 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
43 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
44 42 43 oveq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
45 41 44 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) )
46 45 2ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) )
47 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
48 47 eqeq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 0 ) = 𝑌 ↔ ( 𝐹 ‘ 0 ) = 𝑌 ) )
49 46 48 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑌 ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )
50 49 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑌 ) } ↔ ( 𝐹 ∈ ( 𝐶 ↑m 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )
51 3anass ⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )
52 40 50 51 3bitr4i ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝐶 ↑m 𝐵 ) ∣ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑓 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ⨣ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑌 ) } ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) )
53 36 52 bitrdi ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) → ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )
54 8 53 biadanii ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ 0 ) = 𝑌 ) ) )