Metamath Proof Explorer

Theorem sn-isghm

Description: Longer proof of isghm , unsuccessfully attempting to simplify isghm using elovmpo according to an editorial note (now removed). (Contributed by SN, 7-Jun-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses sn-isghm.w 
|- X = ( Base ` S )
sn-isghm.x 
|- Y = ( Base ` T )
sn-isghm.a 
|- .+ = ( +g ` S )
sn-isghm.b 
|- .+^ = ( +g ` T )
Assertion sn-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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sn-isghm.w 
 |-  X = ( Base ` S )
2 sn-isghm.x 
 |-  Y = ( Base ` T )
3 sn-isghm.a 
 |-  .+ = ( +g ` S )
4 sn-isghm.b 
 |-  .+^ = ( +g ` T )
5 df-ghm 
 |-  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 ) ) ) } )
6 fvex 
 |-  ( Base ` s ) e. _V
7 feq2 
 |-  ( w = ( Base ` s ) -> ( f : w --> ( Base ` t ) <-> f : ( Base ` s ) --> ( Base ` t ) ) )
8 raleq 
 |-  ( 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 ) ) ) )
9 8 raleqbi1dv 
 |-  ( 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 ) ) ) )
10 7 9 anbi12d 
 |-  ( 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 ) ) ) ) )
11 6 10 sbcie 
 |-  ( [. ( 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 ) ) ) )
12 11 abbii 
 |-  { 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 : ( 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 ) ) ) }
13 fvex 
 |-  ( Base ` t ) e. _V
14 fsetex 
 |-  ( ( Base ` t ) e. _V -> { f | f : ( Base ` s ) --> ( Base ` t ) } e. _V )
15 13 14 ax-mp 
 |-  { f | f : ( Base ` s ) --> ( Base ` t ) } e. _V
16 abanssl 
 |-  { f | ( 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 ) ) ) } C_ { f | f : ( Base ` s ) --> ( Base ` t ) }
17 15 16 ssexi 
 |-  { f | ( 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 ) ) ) } e. _V
18 12 17 eqeltri 
 |-  { 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 ) ) ) } e. _V
19 fveq2 
 |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )
20 19 1 eqtr4di 
 |-  ( s = S -> ( Base ` s ) = X )
21 20 adantr 
 |-  ( ( s = S /\ t = T ) -> ( Base ` s ) = X )
22 fveq2 
 |-  ( t = T -> ( Base ` t ) = ( Base ` T ) )
23 22 2 eqtr4di 
 |-  ( t = T -> ( Base ` t ) = Y )
24 23 adantl 
 |-  ( ( s = S /\ t = T ) -> ( Base ` t ) = Y )
25 21 24 feq23d 
 |-  ( ( s = S /\ t = T ) -> ( f : ( Base ` s ) --> ( Base ` t ) <-> f : X --> Y ) )
26 fveq2 
 |-  ( s = S -> ( +g ` s ) = ( +g ` S ) )
27 26 3 eqtr4di 
 |-  ( s = S -> ( +g ` s ) = .+ )
28 27 oveqd 
 |-  ( s = S -> ( u ( +g ` s ) v ) = ( u .+ v ) )
29 28 fveq2d 
 |-  ( s = S -> ( f ` ( u ( +g ` s ) v ) ) = ( f ` ( u .+ v ) ) )
30 fveq2 
 |-  ( t = T -> ( +g ` t ) = ( +g ` T ) )
31 30 4 eqtr4di 
 |-  ( t = T -> ( +g ` t ) = .+^ )
32 31 oveqd 
 |-  ( t = T -> ( ( f ` u ) ( +g ` t ) ( f ` v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) )
33 29 32 eqeqan12d 
 |-  ( ( s = S /\ t = T ) -> ( ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) <-> ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) )
34 21 33 raleqbidv 
 |-  ( ( s = S /\ t = T ) -> ( 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 ) .+^ ( f ` v ) ) ) )
35 21 34 raleqbidv 
 |-  ( ( s = S /\ t = T ) -> ( 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 ) .+^ ( f ` v ) ) ) )
36 25 35 anbi12d 
 |-  ( ( s = S /\ t = T ) -> ( ( 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 --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) ) )
37 36 abbidv 
 |-  ( ( s = S /\ t = T ) -> { f | ( 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 | ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } )
38 12 37 eqtrid 
 |-  ( ( s = S /\ t = T ) -> { 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 --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } )
39 5 18 38 elovmpo 
 |-  ( F e. ( S GrpHom T ) <-> ( S e. Grp /\ T e. Grp /\ F e. { f | ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } ) )
40 1 fvexi 
 |-  X e. _V
41 2 fvexi 
 |-  Y e. _V
42 fex2 
 |-  ( ( F : X --> Y /\ X e. _V /\ Y e. _V ) -> F e. _V )
43 40 41 42 mp3an23 
 |-  ( F : X --> Y -> F e. _V )
44 43 adantr 
 |-  ( ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) -> F e. _V )
45 feq1 
 |-  ( f = F -> ( f : X --> Y <-> F : X --> Y ) )
46 fveq1 
 |-  ( f = F -> ( f ` ( u .+ v ) ) = ( F ` ( u .+ v ) ) )
47 fveq1 
 |-  ( f = F -> ( f ` u ) = ( F ` u ) )
48 fveq1 
 |-  ( f = F -> ( f ` v ) = ( F ` v ) )
49 47 48 oveq12d 
 |-  ( f = F -> ( ( f ` u ) .+^ ( f ` v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) )
50 46 49 eqeq12d 
 |-  ( f = F -> ( ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) <-> ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) )
51 50 2ralbidv 
 |-  ( 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 ) ) ) )
52 45 51 anbi12d 
 |-  ( 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 ) ) ) ) )
53 44 52 elab3 
 |-  ( 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 ) ) ) )
54 53 3anbi3i 
 |-  ( ( S e. Grp /\ T e. Grp /\ F e. { f | ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } ) <-> ( S e. Grp /\ T e. Grp /\ ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) )
55 df-3an 
 |-  ( ( S e. Grp /\ T e. Grp /\ ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) <-> ( ( S e. Grp /\ T e. Grp ) /\ ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) )
56 39 54 55 3bitri 
 |-  ( 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 ) ) ) ) )