MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isghm Structured version   Unicode version

Theorem isghm 16055
Description: Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014.)
Hypotheses
Ref Expression
isghm.w  |-  X  =  ( Base `  S
)
isghm.x  |-  Y  =  ( Base `  T
)
isghm.a  |-  .+  =  ( +g  `  S )
isghm.b  |-  .+^  =  ( +g  `  T )
Assertion
Ref Expression
isghm  |-  ( F  e.  ( S  GrpHom  T )  <->  ( ( S  e.  Grp  /\  T  e.  Grp )  /\  ( F : X --> Y  /\  A. u  e.  X  A. v  e.  X  ( F `  ( u  .+  v ) )  =  ( ( F `  u )  .+^  ( F `
 v ) ) ) ) )
Distinct variable groups:    v, u, S    u, T, v    u, X, v    u,  .+ , v    u, Y, v    u,  .+^ , v    u, F, v

Proof of Theorem isghm
Dummy variables  t 
s  w  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ghm 16053 . . 3  |-  GrpHom  =  ( s  e.  Grp , 
t  e.  Grp  |->  { f  |  [. ( Base `  s )  /  w ]. ( f : w --> ( Base `  t
)  /\  A. u  e.  w  A. v  e.  w  ( f `  ( u ( +g  `  s ) v ) )  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) ) ) } )
21elmpt2cl 6492 . 2  |-  ( F  e.  ( S  GrpHom  T )  ->  ( S  e.  Grp  /\  T  e. 
Grp ) )
3 fvex 5867 . . . . . . . 8  |-  ( Base `  s )  e.  _V
4 feq2 5705 . . . . . . . . 9  |-  ( w  =  ( Base `  s
)  ->  ( f : w --> ( Base `  t )  <->  f :
( Base `  s ) --> ( Base `  t )
) )
5 raleq 3051 . . . . . . . . . 10  |-  ( w  =  ( Base `  s
)  ->  ( A. v  e.  w  (
f `  ( u
( +g  `  s ) v ) )  =  ( ( f `  u ) ( +g  `  t ) ( f `
 v ) )  <->  A. v  e.  ( Base `  s ) ( f `  ( u ( +g  `  s
) v ) )  =  ( ( f `
 u ) ( +g  `  t ) ( f `  v
) ) ) )
65raleqbi1dv 3059 . . . . . . . . 9  |-  ( w  =  ( Base `  s
)  ->  ( A. u  e.  w  A. v  e.  w  (
f `  ( u
( +g  `  s ) v ) )  =  ( ( f `  u ) ( +g  `  t ) ( f `
 v ) )  <->  A. u  e.  ( Base `  s ) A. v  e.  ( Base `  s ) ( f `
 ( u ( +g  `  s ) v ) )  =  ( ( f `  u ) ( +g  `  t ) ( f `
 v ) ) ) )
74, 6anbi12d 710 . . . . . . . 8  |-  ( w  =  ( Base `  s
)  ->  ( (
f : w --> ( Base `  t )  /\  A. u  e.  w  A. v  e.  w  (
f `  ( u
( +g  `  s ) v ) )  =  ( ( f `  u ) ( +g  `  t ) ( f `
 v ) ) )  <->  ( f : ( Base `  s
) --> ( Base `  t
)  /\  A. u  e.  ( Base `  s
) A. v  e.  ( Base `  s
) ( f `  ( u ( +g  `  s ) v ) )  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) ) ) ) )
83, 7sbcie 3359 . . . . . . 7  |-  ( [. ( Base `  s )  /  w ]. ( f : w --> ( Base `  t )  /\  A. u  e.  w  A. v  e.  w  (
f `  ( u
( +g  `  s ) v ) )  =  ( ( f `  u ) ( +g  `  t ) ( f `
 v ) ) )  <->  ( f : ( Base `  s
) --> ( Base `  t
)  /\  A. u  e.  ( Base `  s
) A. v  e.  ( Base `  s
) ( f `  ( u ( +g  `  s ) v ) )  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) ) ) )
9 fveq2 5857 . . . . . . . . . 10  |-  ( s  =  S  ->  ( Base `  s )  =  ( Base `  S
) )
10 isghm.w . . . . . . . . . 10  |-  X  =  ( Base `  S
)
119, 10syl6eqr 2519 . . . . . . . . 9  |-  ( s  =  S  ->  ( Base `  s )  =  X )
1211feq2d 5709 . . . . . . . 8  |-  ( s  =  S  ->  (
f : ( Base `  s ) --> ( Base `  t )  <->  f : X
--> ( Base `  t
) ) )
13 fveq2 5857 . . . . . . . . . . . . . 14  |-  ( s  =  S  ->  ( +g  `  s )  =  ( +g  `  S
) )
14 isghm.a . . . . . . . . . . . . . 14  |-  .+  =  ( +g  `  S )
1513, 14syl6eqr 2519 . . . . . . . . . . . . 13  |-  ( s  =  S  ->  ( +g  `  s )  = 
.+  )
1615oveqd 6292 . . . . . . . . . . . 12  |-  ( s  =  S  ->  (
u ( +g  `  s
) v )  =  ( u  .+  v
) )
1716fveq2d 5861 . . . . . . . . . . 11  |-  ( s  =  S  ->  (
f `  ( u
( +g  `  s ) v ) )  =  ( f `  (
u  .+  v )
) )
1817eqeq1d 2462 . . . . . . . . . 10  |-  ( s  =  S  ->  (
( f `  (
u ( +g  `  s
) v ) )  =  ( ( f `
 u ) ( +g  `  t ) ( f `  v
) )  <->  ( f `  ( u  .+  v
) )  =  ( ( f `  u
) ( +g  `  t
) ( f `  v ) ) ) )
1911, 18raleqbidv 3065 . . . . . . . . 9  |-  ( s  =  S  ->  ( A. v  e.  ( Base `  s ) ( f `  ( u ( +g  `  s
) v ) )  =  ( ( f `
 u ) ( +g  `  t ) ( f `  v
) )  <->  A. v  e.  X  ( f `  ( u  .+  v
) )  =  ( ( f `  u
) ( +g  `  t
) ( f `  v ) ) ) )
2011, 19raleqbidv 3065 . . . . . . . 8  |-  ( s  =  S  ->  ( A. u  e.  ( Base `  s ) A. v  e.  ( Base `  s ) ( f `
 ( u ( +g  `  s ) v ) )  =  ( ( f `  u ) ( +g  `  t ) ( f `
 v ) )  <->  A. u  e.  X  A. v  e.  X  ( f `  (
u  .+  v )
)  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) ) ) )
2112, 20anbi12d 710 . . . . . . 7  |-  ( s  =  S  ->  (
( f : (
Base `  s ) --> ( Base `  t )  /\  A. u  e.  (
Base `  s ) A. v  e.  ( Base `  s ) ( f `  ( u ( +g  `  s
) v ) )  =  ( ( f `
 u ) ( +g  `  t ) ( f `  v
) ) )  <->  ( f : X --> ( Base `  t
)  /\  A. u  e.  X  A. v  e.  X  ( f `  ( u  .+  v
) )  =  ( ( f `  u
) ( +g  `  t
) ( f `  v ) ) ) ) )
228, 21syl5bb 257 . . . . . 6  |-  ( s  =  S  ->  ( [. ( Base `  s
)  /  w ]. ( f : w --> ( Base `  t
)  /\  A. u  e.  w  A. v  e.  w  ( f `  ( u ( +g  `  s ) v ) )  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) ) )  <-> 
( f : X --> ( Base `  t )  /\  A. u  e.  X  A. v  e.  X  ( f `  (
u  .+  v )
)  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) ) ) ) )
2322abbidv 2596 . . . . 5  |-  ( s  =  S  ->  { f  |  [. ( Base `  s )  /  w ]. ( f : w --> ( Base `  t
)  /\  A. u  e.  w  A. v  e.  w  ( f `  ( u ( +g  `  s ) v ) )  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) ) ) }  =  { f  |  ( f : X --> ( Base `  t
)  /\  A. u  e.  X  A. v  e.  X  ( f `  ( u  .+  v
) )  =  ( ( f `  u
) ( +g  `  t
) ( f `  v ) ) ) } )
24 fveq2 5857 . . . . . . . . 9  |-  ( t  =  T  ->  ( Base `  t )  =  ( Base `  T
) )
25 isghm.x . . . . . . . . 9  |-  Y  =  ( Base `  T
)
2624, 25syl6eqr 2519 . . . . . . . 8  |-  ( t  =  T  ->  ( Base `  t )  =  Y )
27 feq3 5706 . . . . . . . 8  |-  ( (
Base `  t )  =  Y  ->  ( f : X --> ( Base `  t )  <->  f : X
--> Y ) )
2826, 27syl 16 . . . . . . 7  |-  ( t  =  T  ->  (
f : X --> ( Base `  t )  <->  f : X
--> Y ) )
29 fveq2 5857 . . . . . . . . . . 11  |-  ( t  =  T  ->  ( +g  `  t )  =  ( +g  `  T
) )
30 isghm.b . . . . . . . . . . 11  |-  .+^  =  ( +g  `  T )
3129, 30syl6eqr 2519 . . . . . . . . . 10  |-  ( t  =  T  ->  ( +g  `  t )  = 
.+^  )
3231oveqd 6292 . . . . . . . . 9  |-  ( t  =  T  ->  (
( f `  u
) ( +g  `  t
) ( f `  v ) )  =  ( ( f `  u )  .+^  ( f `
 v ) ) )
3332eqeq2d 2474 . . . . . . . 8  |-  ( t  =  T  ->  (
( f `  (
u  .+  v )
)  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) )  <->  ( f `  ( u  .+  v
) )  =  ( ( f `  u
)  .+^  ( f `  v ) ) ) )
34332ralbidv 2901 . . . . . . 7  |-  ( t  =  T  ->  ( A. u  e.  X  A. v  e.  X  ( f `  (
u  .+  v )
)  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) )  <->  A. u  e.  X  A. v  e.  X  ( f `  ( u  .+  v
) )  =  ( ( f `  u
)  .+^  ( f `  v ) ) ) )
3528, 34anbi12d 710 . . . . . 6  |-  ( t  =  T  ->  (
( f : X --> ( Base `  t )  /\  A. u  e.  X  A. v  e.  X  ( f `  (
u  .+  v )
)  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) ) )  <-> 
( f : X --> Y  /\  A. u  e.  X  A. v  e.  X  ( f `  ( u  .+  v ) )  =  ( ( f `  u ) 
.+^  ( f `  v ) ) ) ) )
3635abbidv 2596 . . . . 5  |-  ( t  =  T  ->  { f  |  ( f : X --> ( Base `  t
)  /\  A. u  e.  X  A. v  e.  X  ( f `  ( u  .+  v
) )  =  ( ( f `  u
) ( +g  `  t
) ( f `  v ) ) ) }  =  { f  |  ( f : X --> Y  /\  A. u  e.  X  A. v  e.  X  (
f `  ( u  .+  v ) )  =  ( ( f `  u )  .+^  ( f `
 v ) ) ) } )
37 fvex 5867 . . . . . . . 8  |-  ( Base `  S )  e.  _V
3810, 37eqeltri 2544 . . . . . . 7  |-  X  e. 
_V
39 fvex 5867 . . . . . . . 8  |-  ( Base `  T )  e.  _V
4025, 39eqeltri 2544 . . . . . . 7  |-  Y  e. 
_V
41 mapex 7416 . . . . . . 7  |-  ( ( X  e.  _V  /\  Y  e.  _V )  ->  { f  |  f : X --> Y }  e.  _V )
4238, 40, 41mp2an 672 . . . . . 6  |-  { f  |  f : X --> Y }  e.  _V
43 simpl 457 . . . . . . 7  |-  ( ( f : X --> Y  /\  A. u  e.  X  A. v  e.  X  (
f `  ( u  .+  v ) )  =  ( ( f `  u )  .+^  ( f `
 v ) ) )  ->  f : X
--> Y )
4443ss2abi 3565 . . . . . 6  |-  { f  |  ( f : X --> Y  /\  A. u  e.  X  A. v  e.  X  (
f `  ( u  .+  v ) )  =  ( ( f `  u )  .+^  ( f `
 v ) ) ) }  C_  { f  |  f : X --> Y }
4542, 44ssexi 4585 . . . . 5  |-  { f  |  ( f : X --> Y  /\  A. u  e.  X  A. v  e.  X  (
f `  ( u  .+  v ) )  =  ( ( f `  u )  .+^  ( f `
 v ) ) ) }  e.  _V
4623, 36, 1, 45ovmpt2 6413 . . . 4  |-  ( ( S  e.  Grp  /\  T  e.  Grp )  ->  ( S  GrpHom  T )  =  { f  |  ( f : X --> Y  /\  A. u  e.  X  A. v  e.  X  ( f `  ( u  .+  v ) )  =  ( ( f `  u ) 
.+^  ( f `  v ) ) ) } )
4746eleq2d 2530 . . 3  |-  ( ( S  e.  Grp  /\  T  e.  Grp )  ->  ( F  e.  ( S  GrpHom  T )  <->  F  e.  { f  |  ( f : X --> Y  /\  A. u  e.  X  A. v  e.  X  (
f `  ( u  .+  v ) )  =  ( ( f `  u )  .+^  ( f `
 v ) ) ) } ) )
48 fex 6124 . . . . . 6  |-  ( ( F : X --> Y  /\  X  e.  _V )  ->  F  e.  _V )
4938, 48mpan2 671 . . . . 5  |-  ( F : X --> Y  ->  F  e.  _V )
5049adantr 465 . . . 4  |-  ( ( F : X --> Y  /\  A. u  e.  X  A. v  e.  X  ( F `  ( u  .+  v ) )  =  ( ( F `  u )  .+^  ( F `
 v ) ) )  ->  F  e.  _V )
51 feq1 5704 . . . . 5  |-  ( f  =  F  ->  (
f : X --> Y  <->  F : X
--> Y ) )
52 fveq1 5856 . . . . . . 7  |-  ( f  =  F  ->  (
f `  ( u  .+  v ) )  =  ( F `  (
u  .+  v )
) )
53 fveq1 5856 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  u )  =  ( F `  u ) )
54 fveq1 5856 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  v )  =  ( F `  v ) )
5553, 54oveq12d 6293 . . . . . . 7  |-  ( f  =  F  ->  (
( f `  u
)  .+^  ( f `  v ) )  =  ( ( F `  u )  .+^  ( F `
 v ) ) )
5652, 55eqeq12d 2482 . . . . . 6  |-  ( f  =  F  ->  (
( f `  (
u  .+  v )
)  =  ( ( f `  u ) 
.+^  ( f `  v ) )  <->  ( F `  ( u  .+  v
) )  =  ( ( F `  u
)  .+^  ( F `  v ) ) ) )
57562ralbidv 2901 . . . . 5  |-  ( f  =  F  ->  ( A. u  e.  X  A. v  e.  X  ( f `  (
u  .+  v )
)  =  ( ( f `  u ) 
.+^  ( f `  v ) )  <->  A. u  e.  X  A. v  e.  X  ( F `  ( u  .+  v
) )  =  ( ( F `  u
)  .+^  ( F `  v ) ) ) )
5851, 57anbi12d 710 . . . 4  |-  ( f  =  F  ->  (
( f : X --> Y  /\  A. u  e.  X  A. v  e.  X  ( f `  ( u  .+  v ) )  =  ( ( f `  u ) 
.+^  ( f `  v ) ) )  <-> 
( F : X --> Y  /\  A. u  e.  X  A. v  e.  X  ( F `  ( u  .+  v ) )  =  ( ( F `  u ) 
.+^  ( F `  v ) ) ) ) )
5950, 58elab3 3250 . . 3  |-  ( F  e.  { f  |  ( f : X --> Y  /\  A. u  e.  X  A. v  e.  X  ( f `  ( u  .+  v ) )  =  ( ( f `  u ) 
.+^  ( f `  v ) ) ) }  <->  ( F : X
--> Y  /\  A. u  e.  X  A. v  e.  X  ( F `  ( u  .+  v
) )  =  ( ( F `  u
)  .+^  ( F `  v ) ) ) )
6047, 59syl6bb 261 . 2  |-  ( ( S  e.  Grp  /\  T  e.  Grp )  ->  ( F  e.  ( S  GrpHom  T )  <->  ( F : X --> Y  /\  A. u  e.  X  A. v  e.  X  ( F `  ( u  .+  v ) )  =  ( ( F `  u )  .+^  ( F `
 v ) ) ) ) )
612, 60biadan2 642 1  |-  ( F  e.  ( S  GrpHom  T )  <->  ( ( S  e.  Grp  /\  T  e.  Grp )  /\  ( F : X --> Y  /\  A. u  e.  X  A. v  e.  X  ( F `  ( u  .+  v ) )  =  ( ( F `  u )  .+^  ( F `
 v ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    = wceq 1374    e. wcel 1762   {cab 2445   A.wral 2807   _Vcvv 3106   [.wsbc 3324   -->wf 5575   ` cfv 5579  (class class class)co 6275   Basecbs 14479   +g cplusg 14544   Grpcgrp 15716    GrpHom cghm 16052
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-ghm 16053
This theorem is referenced by:  isghm3  16056  ghmgrp1  16057  ghmgrp2  16058  ghmf  16059  ghmlin  16060  isghmd  16064  idghm  16070  ghmf1o  16084  islmhm2  17460  expghm  18289  expghmOLD  18290  mulgghm2  18291  mulgghm2OLD  18294  pi1xfr  21283  pi1coghm  21289  rhmopp  27458
  Copyright terms: Public domain W3C validator