Metamath Proof Explorer


Theorem ismgmhm

Description: Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020)

Ref Expression
Hypotheses ismgmhm.b B = Base S
ismgmhm.c C = Base T
ismgmhm.p + ˙ = + S
ismgmhm.q ˙ = + T
Assertion ismgmhm F S MgmHom T S Mgm T Mgm F : B C x B y B F x + ˙ y = F x ˙ F y

Proof

Step Hyp Ref Expression
1 ismgmhm.b B = Base S
2 ismgmhm.c C = Base T
3 ismgmhm.p + ˙ = + S
4 ismgmhm.q ˙ = + T
5 mgmhmrcl F S MgmHom T S Mgm T Mgm
6 fveq2 t = T Base t = Base T
7 6 2 eqtr4di t = T Base t = C
8 fveq2 s = S Base s = Base S
9 8 1 eqtr4di s = S Base s = B
10 7 9 oveqan12rd s = S t = T Base t Base s = C B
11 9 adantr s = S t = T Base s = B
12 fveq2 s = S + s = + S
13 12 3 eqtr4di s = S + s = + ˙
14 13 oveqd s = S x + s y = x + ˙ y
15 14 fveq2d s = S f x + s y = f x + ˙ y
16 fveq2 t = T + t = + T
17 16 4 eqtr4di t = T + t = ˙
18 17 oveqd t = T f x + t f y = f x ˙ f y
19 15 18 eqeqan12d s = S t = T f x + s y = f x + t f y f x + ˙ y = f x ˙ f y
20 11 19 raleqbidv s = S t = T y Base s f x + s y = f x + t f y y B f x + ˙ y = f x ˙ f y
21 11 20 raleqbidv s = S t = T x Base s y Base s f x + s y = f x + t f y x B y B f x + ˙ y = f x ˙ f y
22 10 21 rabeqbidv s = S t = T f Base t Base s | x Base s y Base s f x + s y = f x + t f y = f C B | x B y B f x + ˙ y = f x ˙ f y
23 df-mgmhm MgmHom = s Mgm , t Mgm f Base t Base s | x Base s y Base s f x + s y = f x + t f y
24 ovex C B V
25 24 rabex f C B | x B y B f x + ˙ y = f x ˙ f y V
26 22 23 25 ovmpoa S Mgm T Mgm S MgmHom T = f C B | x B y B f x + ˙ y = f x ˙ f y
27 26 eleq2d S Mgm T Mgm F S MgmHom T F f C B | x B y B f x + ˙ y = f x ˙ f y
28 fveq1 f = F f x + ˙ y = F x + ˙ y
29 fveq1 f = F f x = F x
30 fveq1 f = F f y = F y
31 29 30 oveq12d f = F f x ˙ f y = F x ˙ F y
32 28 31 eqeq12d f = F f x + ˙ y = f x ˙ f y F x + ˙ y = F x ˙ F y
33 32 2ralbidv f = F x B y B f x + ˙ y = f x ˙ f y x B y B F x + ˙ y = F x ˙ F y
34 33 elrab F f C B | x B y B f x + ˙ y = f x ˙ f y F C B x B y B F x + ˙ y = F x ˙ F y
35 2 fvexi C V
36 1 fvexi B V
37 35 36 elmap F C B F : B C
38 37 anbi1i F C B x B y B F x + ˙ y = F x ˙ F y F : B C x B y B F x + ˙ y = F x ˙ F y
39 34 38 bitri F f C B | x B y B f x + ˙ y = f x ˙ f y F : B C x B y B F x + ˙ y = F x ˙ F y
40 27 39 bitrdi S Mgm T Mgm F S MgmHom T F : B C x B y B F x + ˙ y = F x ˙ F y
41 5 40 biadanii F S MgmHom T S Mgm T Mgm F : B C x B y B F x + ˙ y = F x ˙ F y