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

Theorem isghm 16871
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 16869 . . 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 6522 . 2  |-  ( F  e.  ( S  GrpHom  T )  ->  ( S  e.  Grp  /\  T  e. 
Grp ) )
3 fvex 5888 . . . . . . . 8  |-  ( Base `  s )  e.  _V
4 feq2 5726 . . . . . . . . 9  |-  ( w  =  ( Base `  s
)  ->  ( f : w --> ( Base `  t )  <->  f :
( Base `  s ) --> ( Base `  t )
) )
5 raleq 3025 . . . . . . . . . 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 3033 . . . . . . . . 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 715 . . . . . . . 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 3334 . . . . . . 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 5878 . . . . . . . . . 10  |-  ( s  =  S  ->  ( Base `  s )  =  ( Base `  S
) )
10 isghm.w . . . . . . . . . 10  |-  X  =  ( Base `  S
)
119, 10syl6eqr 2481 . . . . . . . . 9  |-  ( s  =  S  ->  ( Base `  s )  =  X )
1211feq2d 5730 . . . . . . . 8  |-  ( s  =  S  ->  (
f : ( Base `  s ) --> ( Base `  t )  <->  f : X
--> ( Base `  t
) ) )
13 fveq2 5878 . . . . . . . . . . . . . 14  |-  ( s  =  S  ->  ( +g  `  s )  =  ( +g  `  S
) )
14 isghm.a . . . . . . . . . . . . . 14  |-  .+  =  ( +g  `  S )
1513, 14syl6eqr 2481 . . . . . . . . . . . . 13  |-  ( s  =  S  ->  ( +g  `  s )  = 
.+  )
1615oveqd 6319 . . . . . . . . . . . 12  |-  ( s  =  S  ->  (
u ( +g  `  s
) v )  =  ( u  .+  v
) )
1716fveq2d 5882 . . . . . . . . . . 11  |-  ( s  =  S  ->  (
f `  ( u
( +g  `  s ) v ) )  =  ( f `  (
u  .+  v )
) )
1817eqeq1d 2424 . . . . . . . . . 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 3039 . . . . . . . . 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 3039 . . . . . . . 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 715 . . . . . . 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 260 . . . . . 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 2558 . . . . 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 5878 . . . . . . . . 9  |-  ( t  =  T  ->  ( Base `  t )  =  ( Base `  T
) )
25 isghm.x . . . . . . . . 9  |-  Y  =  ( Base `  T
)
2624, 25syl6eqr 2481 . . . . . . . 8  |-  ( t  =  T  ->  ( Base `  t )  =  Y )
2726feq3d 5731 . . . . . . 7  |-  ( t  =  T  ->  (
f : X --> ( Base `  t )  <->  f : X
--> Y ) )
28 fveq2 5878 . . . . . . . . . . 11  |-  ( t  =  T  ->  ( +g  `  t )  =  ( +g  `  T
) )
29 isghm.b . . . . . . . . . . 11  |-  .+^  =  ( +g  `  T )
3028, 29syl6eqr 2481 . . . . . . . . . 10  |-  ( t  =  T  ->  ( +g  `  t )  = 
.+^  )
3130oveqd 6319 . . . . . . . . 9  |-  ( t  =  T  ->  (
( f `  u
) ( +g  `  t
) ( f `  v ) )  =  ( ( f `  u )  .+^  ( f `
 v ) ) )
3231eqeq2d 2436 . . . . . . . 8  |-  ( t  =  T  ->  (
( f `  (
u  .+  v )
)  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) )  <->  ( f `  ( u  .+  v
) )  =  ( ( f `  u
)  .+^  ( f `  v ) ) ) )
33322ralbidv 2869 . . . . . . 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 ) ) ) )
3427, 33anbi12d 715 . . . . . 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 ) ) ) ) )
3534abbidv 2558 . . . . 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 ) ) ) } )
36 fvex 5888 . . . . . . . 8  |-  ( Base `  S )  e.  _V
3710, 36eqeltri 2506 . . . . . . 7  |-  X  e. 
_V
38 fvex 5888 . . . . . . . 8  |-  ( Base `  T )  e.  _V
3925, 38eqeltri 2506 . . . . . . 7  |-  Y  e. 
_V
40 mapex 7483 . . . . . . 7  |-  ( ( X  e.  _V  /\  Y  e.  _V )  ->  { f  |  f : X --> Y }  e.  _V )
4137, 39, 40mp2an 676 . . . . . 6  |-  { f  |  f : X --> Y }  e.  _V
42 simpl 458 . . . . . . 7  |-  ( ( f : X --> Y  /\  A. u  e.  X  A. v  e.  X  (
f `  ( u  .+  v ) )  =  ( ( f `  u )  .+^  ( f `
 v ) ) )  ->  f : X
--> Y )
4342ss2abi 3533 . . . . . 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 }
4441, 43ssexi 4566 . . . . 5  |-  { f  |  ( f : X --> Y  /\  A. u  e.  X  A. v  e.  X  (
f `  ( u  .+  v ) )  =  ( ( f `  u )  .+^  ( f `
 v ) ) ) }  e.  _V
4523, 35, 1, 44ovmpt2 6443 . . . 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 ) ) ) } )
4645eleq2d 2492 . . 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 ) ) ) } ) )
47 fex 6150 . . . . . 6  |-  ( ( F : X --> Y  /\  X  e.  _V )  ->  F  e.  _V )
4837, 47mpan2 675 . . . . 5  |-  ( F : X --> Y  ->  F  e.  _V )
4948adantr 466 . . . 4  |-  ( ( F : X --> Y  /\  A. u  e.  X  A. v  e.  X  ( F `  ( u  .+  v ) )  =  ( ( F `  u )  .+^  ( F `
 v ) ) )  ->  F  e.  _V )
50 feq1 5725 . . . . 5  |-  ( f  =  F  ->  (
f : X --> Y  <->  F : X
--> Y ) )
51 fveq1 5877 . . . . . . 7  |-  ( f  =  F  ->  (
f `  ( u  .+  v ) )  =  ( F `  (
u  .+  v )
) )
52 fveq1 5877 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  u )  =  ( F `  u ) )
53 fveq1 5877 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  v )  =  ( F `  v ) )
5452, 53oveq12d 6320 . . . . . . 7  |-  ( f  =  F  ->  (
( f `  u
)  .+^  ( f `  v ) )  =  ( ( F `  u )  .+^  ( F `
 v ) ) )
5551, 54eqeq12d 2444 . . . . . 6  |-  ( f  =  F  ->  (
( f `  (
u  .+  v )
)  =  ( ( f `  u ) 
.+^  ( f `  v ) )  <->  ( F `  ( u  .+  v
) )  =  ( ( F `  u
)  .+^  ( F `  v ) ) ) )
56552ralbidv 2869 . . . . 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 ) ) ) )
5750, 56anbi12d 715 . . . 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 ) ) ) ) )
5849, 57elab3 3225 . . 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 ) ) ) )
5946, 58syl6bb 264 . 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 ) ) ) ) )
602, 59biadan2 646 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 187    /\ wa 370    = wceq 1437    e. wcel 1868   {cab 2407   A.wral 2775   _Vcvv 3081   [.wsbc 3299   -->wf 5594   ` cfv 5598  (class class class)co 6302   Basecbs 15109   +g cplusg 15178   Grpcgrp 16657    GrpHom cghm 16868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-ghm 16869
This theorem is referenced by:  isghm3  16872  ghmgrp1  16873  ghmgrp2  16874  ghmf  16875  ghmlin  16876  isghmd  16880  idghm  16886  ghmf1o  16900  islmhm2  18249  expghm  19054  mulgghm2  19055  pi1xfr  22073  pi1coghm  22079  rhmopp  28578  isrnghm  39164
  Copyright terms: Public domain W3C validator