Metamath Proof Explorer

Definition df-mhm

Description: A monoid homomorphism is a function on the base sets which preserves the binary operation and the identity. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Assertion df-mhm MndHom = ( 𝑠 ∈ Mnd , 𝑡 ∈ Mnd ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 0g ‘ 𝑡 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmhm ⊢ MndHom
1 vs ⊢ 𝑠
2 cmnd ⊢ Mnd
3 vt ⊢ 𝑡
4 vf ⊢ 𝑓
5 cbs ⊢ Base
6 3 cv ⊢ 𝑡
7 6 5 cfv ⊢ ( Base ‘ 𝑡 )
8 cmap ⊢ ↑m
9 1 cv ⊢ 𝑠
10 9 5 cfv ⊢ ( Base ‘ 𝑠 )
11 7 10 8 co ⊢ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) )
12 vx ⊢ 𝑥
13 vy ⊢ 𝑦
14 4 cv ⊢ 𝑓
15 12 cv ⊢ 𝑥
16 cplusg ⊢ +g
17 9 16 cfv ⊢ ( +g ‘ 𝑠 )
18 13 cv ⊢ 𝑦
19 15 18 17 co ⊢ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 )
20 19 14 cfv ⊢ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) )
21 15 14 cfv ⊢ ( 𝑓 ‘ 𝑥 )
22 6 16 cfv ⊢ ( +g ‘ 𝑡 )
23 18 14 cfv ⊢ ( 𝑓 ‘ 𝑦 )
24 21 23 22 co ⊢ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
25 20 24 wceq ⊢ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
26 25 13 10 wral ⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
27 26 12 10 wral ⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
28 c0g ⊢ 0g
29 9 28 cfv ⊢ ( 0g ‘ 𝑠 )
30 29 14 cfv ⊢ ( 𝑓 ‘ ( 0g ‘ 𝑠 ) )
31 6 28 cfv ⊢ ( 0g ‘ 𝑡 )
32 30 31 wceq ⊢ ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 0g ‘ 𝑡 )
33 27 32 wa ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 0g ‘ 𝑡 ) )
34 33 4 11 crab ⊢ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 0g ‘ 𝑡 ) ) }
35 1 3 2 2 34 cmpo ⊢ ( 𝑠 ∈ Mnd , 𝑡 ∈ Mnd ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 0g ‘ 𝑡 ) ) } )
36 0 35 wceq ⊢ MndHom = ( 𝑠 ∈ Mnd , 𝑡 ∈ Mnd ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑠 ) ) = ( 0g ‘ 𝑡 ) ) } )