Metamath Proof Explorer


Theorem isghm

Description: Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Hypotheses isghm.w X = Base S
isghm.x Y = Base T
isghm.a + ˙ = + S
isghm.b ˙ = + T
Assertion isghm F S GrpHom T S Grp T Grp F : X Y u X v X F u + ˙ v = F u ˙ F v

Proof

Step Hyp Ref Expression
1 isghm.w X = Base S
2 isghm.x Y = Base T
3 isghm.a + ˙ = + S
4 isghm.b ˙ = + T
5 df-ghm GrpHom = s Grp , t Grp f | [˙Base s / w]˙ f : w Base t u w v w f u + s v = f u + t f v
6 5 elmpocl F S GrpHom T S Grp T Grp
7 fvex Base s V
8 feq2 w = Base s f : w Base t f : Base s Base t
9 raleq w = Base s v w f u + s v = f u + t f v v Base s f u + s v = f u + t f v
10 9 raleqbi1dv w = Base s u w v w f u + s v = f u + t f v u Base s v Base s f u + s v = f u + t f v
11 8 10 anbi12d w = Base s f : w Base t u w v w f u + s v = f u + t f v f : Base s Base t u Base s v Base s f u + s v = f u + t f v
12 7 11 sbcie [˙Base s / w]˙ f : w Base t u w v w f u + s v = f u + t f v f : Base s Base t u Base s v Base s f u + s v = f u + t f v
13 fveq2 s = S Base s = Base S
14 13 1 eqtr4di s = S Base s = X
15 14 feq2d s = S f : Base s Base t f : X Base t
16 fveq2 s = S + s = + S
17 16 3 eqtr4di s = S + s = + ˙
18 17 oveqd s = S u + s v = u + ˙ v
19 18 fveqeq2d s = S f u + s v = f u + t f v f u + ˙ v = f u + t f v
20 14 19 raleqbidv s = S v Base s f u + s v = f u + t f v v X f u + ˙ v = f u + t f v
21 14 20 raleqbidv s = S u Base s v Base s f u + s v = f u + t f v u X v X f u + ˙ v = f u + t f v
22 15 21 anbi12d s = S f : Base s Base t u Base s v Base s f u + s v = f u + t f v f : X Base t u X v X f u + ˙ v = f u + t f v
23 12 22 syl5bb s = S [˙Base s / w]˙ f : w Base t u w v w f u + s v = f u + t f v f : X Base t u X v X f u + ˙ v = f u + t f v
24 23 abbidv s = S f | [˙Base s / w]˙ f : w Base t u w v w f u + s v = f u + t f v = f | f : X Base t u X v X f u + ˙ v = f u + t f v
25 fveq2 t = T Base t = Base T
26 25 2 eqtr4di t = T Base t = Y
27 26 feq3d t = T f : X Base t f : X Y
28 fveq2 t = T + t = + T
29 28 4 eqtr4di t = T + t = ˙
30 29 oveqd t = T f u + t f v = f u ˙ f v
31 30 eqeq2d t = T f u + ˙ v = f u + t f v f u + ˙ v = f u ˙ f v
32 31 2ralbidv t = T u X v X f u + ˙ v = f u + t f v u X v X f u + ˙ v = f u ˙ f v
33 27 32 anbi12d t = T f : X Base t u X v X f u + ˙ v = f u + t f v f : X Y u X v X f u + ˙ v = f u ˙ f v
34 33 abbidv t = T f | f : X Base t u X v X f u + ˙ v = f u + t f v = f | f : X Y u X v X f u + ˙ v = f u ˙ f v
35 1 fvexi X V
36 2 fvexi Y V
37 mapex X V Y V f | f : X Y V
38 35 36 37 mp2an f | f : X Y V
39 simpl f : X Y u X v X f u + ˙ v = f u ˙ f v f : X Y
40 39 ss2abi f | f : X Y u X v X f u + ˙ v = f u ˙ f v f | f : X Y
41 38 40 ssexi f | f : X Y u X v X f u + ˙ v = f u ˙ f v V
42 24 34 5 41 ovmpo S Grp T Grp S GrpHom T = f | f : X Y u X v X f u + ˙ v = f u ˙ f v
43 42 eleq2d S Grp T Grp F S GrpHom T F f | f : X Y u X v X f u + ˙ v = f u ˙ f v
44 fex F : X Y X V F V
45 35 44 mpan2 F : X Y F V
46 45 adantr F : X Y u X v X F u + ˙ v = F u ˙ F v F V
47 feq1 f = F f : X Y F : X Y
48 fveq1 f = F f u + ˙ v = F u + ˙ v
49 fveq1 f = F f u = F u
50 fveq1 f = F f v = F v
51 49 50 oveq12d f = F f u ˙ f v = F u ˙ F v
52 48 51 eqeq12d f = F f u + ˙ v = f u ˙ f v F u + ˙ v = F u ˙ F v
53 52 2ralbidv f = F u X v X f u + ˙ v = f u ˙ f v u X v X F u + ˙ v = F u ˙ F v
54 47 53 anbi12d f = F f : X Y u X v X f u + ˙ v = f u ˙ f v F : X Y u X v X F u + ˙ v = F u ˙ F v
55 46 54 elab3 F f | f : X Y u X v X f u + ˙ v = f u ˙ f v F : X Y u X v X F u + ˙ v = F u ˙ F v
56 43 55 bitrdi S Grp T Grp F S GrpHom T F : X Y u X v X F u + ˙ v = F u ˙ F v
57 6 56 biadanii F S GrpHom T S Grp T Grp F : X Y u X v X F u + ˙ v = F u ˙ F v