This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elghomlem1OLD

Description: Obsolete as of 15-Mar-2020. Lemma for elghomOLD . (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis elghomlem1OLD.1 
|- S = { f | ( f : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) }
Assertion elghomlem1OLD 
|- ( ( G e. GrpOp /\ H e. GrpOp ) -> ( G GrpOpHom H ) = S )

Proof

Step Hyp Ref Expression
1 elghomlem1OLD.1 
 |-  S = { f | ( f : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) }
2 rnexg 
 |-  ( G e. GrpOp -> ran G e. _V )
3 rnexg 
 |-  ( H e. GrpOp -> ran H e. _V )
4 1 fabexg 
 |-  ( ( ran G e. _V /\ ran H e. _V ) -> S e. _V )
5 2 3 4 syl2an 
 |-  ( ( G e. GrpOp /\ H e. GrpOp ) -> S e. _V )
6 rneq 
 |-  ( g = G -> ran g = ran G )
7 6 feq2d 
 |-  ( g = G -> ( f : ran g --> ran h <-> f : ran G --> ran h ) )
8 oveq 
 |-  ( g = G -> ( x g y ) = ( x G y ) )
9 8 fveq2d 
 |-  ( g = G -> ( f ` ( x g y ) ) = ( f ` ( x G y ) ) )
10 9 eqeq2d 
 |-  ( g = G -> ( ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) <-> ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x G y ) ) ) )
11 6 10 raleqbidv 
 |-  ( g = G -> ( A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) <-> A. y e. ran G ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x G y ) ) ) )
12 6 11 raleqbidv 
 |-  ( g = G -> ( A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) <-> A. x e. ran G A. y e. ran G ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x G y ) ) ) )
13 7 12 anbi12d 
 |-  ( g = G -> ( ( f : ran g --> ran h /\ A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) ) <-> ( f : ran G --> ran h /\ A. x e. ran G A. y e. ran G ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x G y ) ) ) ) )
14 13 abbidv 
 |-  ( g = G -> { f | ( f : ran g --> ran h /\ A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) ) } = { f | ( f : ran G --> ran h /\ A. x e. ran G A. y e. ran G ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x G y ) ) ) } )
15 rneq 
 |-  ( h = H -> ran h = ran H )
16 15 feq3d 
 |-  ( h = H -> ( f : ran G --> ran h <-> f : ran G --> ran H ) )
17 oveq 
 |-  ( h = H -> ( ( f ` x ) h ( f ` y ) ) = ( ( f ` x ) H ( f ` y ) ) )
18 17 eqeq1d 
 |-  ( h = H -> ( ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x G y ) ) <-> ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) )
19 18 2ralbidv 
 |-  ( h = H -> ( A. x e. ran G A. y e. ran G ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x G y ) ) <-> A. x e. ran G A. y e. ran G ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) )
20 16 19 anbi12d 
 |-  ( h = H -> ( ( f : ran G --> ran h /\ A. x e. ran G A. y e. ran G ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x G y ) ) ) <-> ( f : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) ) )
21 20 abbidv 
 |-  ( h = H -> { f | ( f : ran G --> ran h /\ A. x e. ran G A. y e. ran G ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x G y ) ) ) } = { f | ( f : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) } )
22 21 1 eqtr4di 
 |-  ( h = H -> { f | ( f : ran G --> ran h /\ A. x e. ran G A. y e. ran G ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x G y ) ) ) } = S )
23 df-ghomOLD 
 |-  GrpOpHom = ( g e. GrpOp , h e. GrpOp |-> { f | ( f : ran g --> ran h /\ A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) ) } )
24 14 22 23 ovmpog 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ S e. _V ) -> ( G GrpOpHom H ) = S )
25 5 24 mpd3an3 
 |-  ( ( G e. GrpOp /\ H e. GrpOp ) -> ( G GrpOpHom H ) = S )