Metamath Proof Explorer


Theorem ismhm

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

Ref Expression
Hypotheses ismhm.b B = Base S
ismhm.c C = Base T
ismhm.p + ˙ = + S
ismhm.q ˙ = + T
ismhm.z 0 ˙ = 0 S
ismhm.y Y = 0 T
Assertion ismhm F S MndHom T S Mnd T Mnd F : B C x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Y

Proof

Step Hyp Ref Expression
1 ismhm.b B = Base S
2 ismhm.c C = Base T
3 ismhm.p + ˙ = + S
4 ismhm.q ˙ = + T
5 ismhm.z 0 ˙ = 0 S
6 ismhm.y Y = 0 T
7 df-mhm MndHom = s Mnd , t Mnd f Base t Base s | x Base s y Base s f x + s y = f x + t f y f 0 s = 0 t
8 7 elmpocl F S MndHom T S Mnd T Mnd
9 fveq2 t = T Base t = Base T
10 9 2 eqtr4di t = T Base t = C
11 fveq2 s = S Base s = Base S
12 11 1 eqtr4di s = S Base s = B
13 10 12 oveqan12rd s = S t = T Base t Base s = C B
14 12 adantr s = S t = T Base s = B
15 fveq2 s = S + s = + S
16 15 3 eqtr4di s = S + s = + ˙
17 16 oveqd s = S x + s y = x + ˙ y
18 17 fveq2d s = S f x + s y = f x + ˙ y
19 fveq2 t = T + t = + T
20 19 4 eqtr4di t = T + t = ˙
21 20 oveqd t = T f x + t f y = f x ˙ f y
22 18 21 eqeqan12d s = S t = T f x + s y = f x + t f y f x + ˙ y = f x ˙ f y
23 14 22 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
24 14 23 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
25 fveq2 s = S 0 s = 0 S
26 25 5 eqtr4di s = S 0 s = 0 ˙
27 26 fveq2d s = S f 0 s = f 0 ˙
28 fveq2 t = T 0 t = 0 T
29 28 6 eqtr4di t = T 0 t = Y
30 27 29 eqeqan12d s = S t = T f 0 s = 0 t f 0 ˙ = Y
31 24 30 anbi12d s = S t = T x Base s y Base s f x + s y = f x + t f y f 0 s = 0 t x B y B f x + ˙ y = f x ˙ f y f 0 ˙ = Y
32 13 31 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 0 s = 0 t = f C B | x B y B f x + ˙ y = f x ˙ f y f 0 ˙ = Y
33 ovex C B V
34 33 rabex f C B | x B y B f x + ˙ y = f x ˙ f y f 0 ˙ = Y V
35 32 7 34 ovmpoa S Mnd T Mnd S MndHom T = f C B | x B y B f x + ˙ y = f x ˙ f y f 0 ˙ = Y
36 35 eleq2d S Mnd T Mnd F S MndHom T F f C B | x B y B f x + ˙ y = f x ˙ f y f 0 ˙ = Y
37 2 fvexi C V
38 1 fvexi B V
39 37 38 elmap F C B F : B C
40 39 anbi1i F C B x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Y F : B C x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Y
41 fveq1 f = F f x + ˙ y = F x + ˙ y
42 fveq1 f = F f x = F x
43 fveq1 f = F f y = F y
44 42 43 oveq12d f = F f x ˙ f y = F x ˙ F y
45 41 44 eqeq12d f = F f x + ˙ y = f x ˙ f y F x + ˙ y = F x ˙ F y
46 45 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
47 fveq1 f = F f 0 ˙ = F 0 ˙
48 47 eqeq1d f = F f 0 ˙ = Y F 0 ˙ = Y
49 46 48 anbi12d f = F x B y B f x + ˙ y = f x ˙ f y f 0 ˙ = Y x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Y
50 49 elrab F f C B | x B y B f x + ˙ y = f x ˙ f y f 0 ˙ = Y F C B x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Y
51 3anass F : B C x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Y F : B C x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Y
52 40 50 51 3bitr4i F f C B | x B y B f x + ˙ y = f x ˙ f y f 0 ˙ = Y F : B C x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Y
53 36 52 bitrdi S Mnd T Mnd F S MndHom T F : B C x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Y
54 8 53 biadanii F S MndHom T S Mnd T Mnd F : B C x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Y