Metamath Proof Explorer

Definition df-bj-mgmhom

Description: Define the set of magma morphisms between two magmas. If domain and codomain are semigroups, monoids, or groups, then one obtains the set of morphisms of these structures. (Contributed by BJ, 10-Feb-2022)

Ref Expression
Assertion df-bj-mgmhom ⊢ ⟶Mgm = x ∈ Mgm , y ∈ Mgm ⟼ f ∈ Base x ⟶Set Base y | ∀ u ∈ Base x ∀ v ∈ Base x f ⁡ u + x v = f ⁡ u + y f ⁡ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgmhom class ⟶Mgm
1 vx setvar x
2 cmgm class Mgm
3 vy setvar y
4 vf setvar f
5 cbs class Base
6 1 cv setvar x
7 6 5 cfv class Base x
8 csethom class ⟶Set
9 3 cv setvar y
10 9 5 cfv class Base y
11 7 10 8 co class Base x ⟶Set Base y
12 vu setvar u
13 vv setvar v
14 4 cv setvar f
15 12 cv setvar u
16 cplusg class + 𝑔
17 6 16 cfv class + x
18 13 cv setvar v
19 15 18 17 co class u + x v
20 19 14 cfv class f ⁡ u + x v
21 15 14 cfv class f ⁡ u
22 9 16 cfv class + y
23 18 14 cfv class f ⁡ v
24 21 23 22 co class f ⁡ u + y f ⁡ v
25 20 24 wceq wff f ⁡ u + x v = f ⁡ u + y f ⁡ v
26 25 13 7 wral wff ∀ v ∈ Base x f ⁡ u + x v = f ⁡ u + y f ⁡ v
27 26 12 7 wral wff ∀ u ∈ Base x ∀ v ∈ Base x f ⁡ u + x v = f ⁡ u + y f ⁡ v
28 27 4 11 crab class f ∈ Base x ⟶Set Base y | ∀ u ∈ Base x ∀ v ∈ Base x f ⁡ u + x v = f ⁡ u + y f ⁡ v
29 1 3 2 2 28 cmpo class x ∈ Mgm , y ∈ Mgm ⟼ f ∈ Base x ⟶Set Base y | ∀ u ∈ Base x ∀ v ∈ Base x f ⁡ u + x v = f ⁡ u + y f ⁡ v
30 0 29 wceq wff ⟶Mgm = x ∈ Mgm , y ∈ Mgm ⟼ f ∈ Base x ⟶Set Base y | ∀ u ∈ Base x ∀ v ∈ Base x f ⁡ u + x v = f ⁡ u + y f ⁡ v