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

Theorem isghm 15736
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 15734 . . 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 6299 . 2  |-  ( F  e.  ( S  GrpHom  T )  ->  ( S  e.  Grp  /\  T  e. 
Grp ) )
3 fvex 5694 . . . . . . . 8  |-  ( Base `  s )  e.  _V
4 feq2 5536 . . . . . . . . 9  |-  ( w  =  ( Base `  s
)  ->  ( f : w --> ( Base `  t )  <->  f :
( Base `  s ) --> ( Base `  t )
) )
5 raleq 2911 . . . . . . . . . 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 2919 . . . . . . . . 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 3214 . . . . . . 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 5684 . . . . . . . . . 10  |-  ( s  =  S  ->  ( Base `  s )  =  ( Base `  S
) )
10 isghm.w . . . . . . . . . 10  |-  X  =  ( Base `  S
)
119, 10syl6eqr 2487 . . . . . . . . 9  |-  ( s  =  S  ->  ( Base `  s )  =  X )
1211feq2d 5540 . . . . . . . 8  |-  ( s  =  S  ->  (
f : ( Base `  s ) --> ( Base `  t )  <->  f : X
--> ( Base `  t
) ) )
13 fveq2 5684 . . . . . . . . . . . . . 14  |-  ( s  =  S  ->  ( +g  `  s )  =  ( +g  `  S
) )
14 isghm.a . . . . . . . . . . . . . 14  |-  .+  =  ( +g  `  S )
1513, 14syl6eqr 2487 . . . . . . . . . . . . 13  |-  ( s  =  S  ->  ( +g  `  s )  = 
.+  )
1615oveqd 6103 . . . . . . . . . . . 12  |-  ( s  =  S  ->  (
u ( +g  `  s
) v )  =  ( u  .+  v
) )
1716fveq2d 5688 . . . . . . . . . . 11  |-  ( s  =  S  ->  (
f `  ( u
( +g  `  s ) v ) )  =  ( f `  (
u  .+  v )
) )
1817eqeq1d 2445 . . . . . . . . . 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 2925 . . . . . . . . 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 2925 . . . . . . . 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 2551 . . . . 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 5684 . . . . . . . . 9  |-  ( t  =  T  ->  ( Base `  t )  =  ( Base `  T
) )
25 isghm.x . . . . . . . . 9  |-  Y  =  ( Base `  T
)
2624, 25syl6eqr 2487 . . . . . . . 8  |-  ( t  =  T  ->  ( Base `  t )  =  Y )
27 feq3 5537 . . . . . . . 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 5684 . . . . . . . . . . 11  |-  ( t  =  T  ->  ( +g  `  t )  =  ( +g  `  T
) )
30 isghm.b . . . . . . . . . . 11  |-  .+^  =  ( +g  `  T )
3129, 30syl6eqr 2487 . . . . . . . . . 10  |-  ( t  =  T  ->  ( +g  `  t )  = 
.+^  )
3231oveqd 6103 . . . . . . . . 9  |-  ( t  =  T  ->  (
( f `  u
) ( +g  `  t
) ( f `  v ) )  =  ( ( f `  u )  .+^  ( f `
 v ) ) )
3332eqeq2d 2448 . . . . . . . 8  |-  ( t  =  T  ->  (
( f `  (
u  .+  v )
)  =  ( ( f `  u ) ( +g  `  t
) ( f `  v ) )  <->  ( f `  ( u  .+  v
) )  =  ( ( f `  u
)  .+^  ( f `  v ) ) ) )
34332ralbidv 2751 . . . . . . 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 2551 . . . . 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 5694 . . . . . . . 8  |-  ( Base `  S )  e.  _V
3810, 37eqeltri 2507 . . . . . . 7  |-  X  e. 
_V
39 fvex 5694 . . . . . . . 8  |-  ( Base `  T )  e.  _V
4025, 39eqeltri 2507 . . . . . . 7  |-  Y  e. 
_V
41 mapex 7212 . . . . . . 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 3417 . . . . . 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 4430 . . . . 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 6221 . . . 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 2504 . . 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 5943 . . . . . 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 5535 . . . . 5  |-  ( f  =  F  ->  (
f : X --> Y  <->  F : X
--> Y ) )
52 fveq1 5683 . . . . . . 7  |-  ( f  =  F  ->  (
f `  ( u  .+  v ) )  =  ( F `  (
u  .+  v )
) )
53 fveq1 5683 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  u )  =  ( F `  u ) )
54 fveq1 5683 . . . . . . . 8  |-  ( f  =  F  ->  (
f `  v )  =  ( F `  v ) )
5553, 54oveq12d 6104 . . . . . . 7  |-  ( f  =  F  ->  (
( f `  u
)  .+^  ( f `  v ) )  =  ( ( F `  u )  .+^  ( F `
 v ) ) )
5652, 55eqeq12d 2451 . . . . . 6  |-  ( f  =  F  ->  (
( f `  (
u  .+  v )
)  =  ( ( f `  u ) 
.+^  ( f `  v ) )  <->  ( F `  ( u  .+  v
) )  =  ( ( F `  u
)  .+^  ( F `  v ) ) ) )
57562ralbidv 2751 . . . . 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 3106 . . 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 1369    e. wcel 1756   {cab 2423   A.wral 2709   _Vcvv 2966   [.wsbc 3179   -->wf 5407   ` cfv 5411  (class class class)co 6086   Basecbs 14166   +g cplusg 14230   Grpcgrp 15402    GrpHom cghm 15733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-iun 4166  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-ghm 15734
This theorem is referenced by:  isghm3  15737  ghmgrp1  15738  ghmgrp2  15739  ghmf  15740  ghmlin  15741  isghmd  15745  idghm  15751  ghmf1o  15765  islmhm2  17093  expghm  17892  expghmOLD  17893  mulgghm2  17894  mulgghm2OLD  17897  pi1xfr  20596  pi1coghm  20602  rhmopp  26234
  Copyright terms: Public domain W3C validator