This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-mgmhm

Description: A magma homomorphism is a function on the base sets which preserves the binary operation. (Contributed by AV, 24-Feb-2020)

Ref Expression
Assertion df-mgmhm MgmHom = ( 𝑠 ∈ Mgm , 𝑡 ∈ Mgm ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgmhm ⊢ MgmHom
1 vs ⊢ 𝑠
2 cmgm ⊢ Mgm
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 27 4 11 crab ⊢ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) }
29 1 3 2 2 28 cmpo ⊢ ( 𝑠 ∈ Mgm , 𝑡 ∈ Mgm ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) } )
30 0 29 wceq ⊢ MgmHom = ( 𝑠 ∈ Mgm , 𝑡 ∈ Mgm ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) } )