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

Metamath Proof Explorer

Theorem elghomlem2OLD

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 elghomlem2OLD 
|- ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom 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 ) ) ) ) )

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 1 elghomlem1OLD 
 |-  ( ( G e. GrpOp /\ H e. GrpOp ) -> ( G GrpOpHom H ) = S )
3 2 eleq2d 
 |-  ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom H ) <-> F e. S ) )
4 elex 
 |-  ( F e. S -> F e. _V )
5 feq1 
 |-  ( f = F -> ( f : ran G --> ran H <-> F : ran G --> ran H ) )
6 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
7 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
8 6 7 oveq12d 
 |-  ( f = F -> ( ( f ` x ) H ( f ` y ) ) = ( ( F ` x ) H ( F ` y ) ) )
9 fveq1 
 |-  ( f = F -> ( f ` ( x G y ) ) = ( F ` ( x G y ) ) )
10 8 9 eqeq12d 
 |-  ( f = F -> ( ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) <-> ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) )
11 10 2ralbidv 
 |-  ( f = F -> ( 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 ) ) ) )
12 5 11 anbi12d 
 |-  ( f = 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 : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )
13 12 1 elab2g 
 |-  ( F e. _V -> ( F e. S <-> ( 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 biimpd 
 |-  ( F e. _V -> ( F e. S -> ( 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 4 14 mpcom 
 |-  ( F e. S -> ( F : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) )
16 rnexg 
 |-  ( G e. GrpOp -> ran G e. _V )
17 fex 
 |-  ( ( F : ran G --> ran H /\ ran G e. _V ) -> F e. _V )
18 17 expcom 
 |-  ( ran G e. _V -> ( F : ran G --> ran H -> F e. _V ) )
19 16 18 syl 
 |-  ( G e. GrpOp -> ( F : ran G --> ran H -> F e. _V ) )
20 19 adantrd 
 |-  ( G e. GrpOp -> ( ( 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 e. _V ) )
21 13 biimprd 
 |-  ( F e. _V -> ( ( 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 e. S ) )
22 20 21 syli 
 |-  ( G e. GrpOp -> ( ( 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 e. S ) )
23 15 22 impbid2 
 |-  ( G e. GrpOp -> ( F e. S <-> ( 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 23 adantr 
 |-  ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. S <-> ( F : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )
25 3 24 bitrd 
 |-  ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom 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 ) ) ) ) )