Metamath Proof Explorer

Theorem isrngohom

Description: The predicate "is a ring homomorphism from R to S ". (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses rnghomval.1 
|- G = ( 1st ` R )
rnghomval.2 
|- H = ( 2nd ` R )
rnghomval.3 
|- X = ran G
rnghomval.4 
|- U = ( GId ` H )
rnghomval.5 
|- J = ( 1st ` S )
rnghomval.6 
|- K = ( 2nd ` S )
rnghomval.7 
|- Y = ran J
rnghomval.8 
|- V = ( GId ` K )
Assertion isrngohom 
|- ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RngHom S ) <-> ( F : X --> Y /\ ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rnghomval.1 
 |-  G = ( 1st ` R )
2 rnghomval.2 
 |-  H = ( 2nd ` R )
3 rnghomval.3 
 |-  X = ran G
4 rnghomval.4 
 |-  U = ( GId ` H )
5 rnghomval.5 
 |-  J = ( 1st ` S )
6 rnghomval.6 
 |-  K = ( 2nd ` S )
7 rnghomval.7 
 |-  Y = ran J
8 rnghomval.8 
 |-  V = ( GId ` K )
9 1 2 3 4 5 6 7 8 rngohomval 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( R RngHom S ) = { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } )
10 9 eleq2d 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RngHom S ) <-> F e. { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } ) )
11 5 fvexi 
 |-  J e. _V
12 11 rnex 
 |-  ran J e. _V
13 7 12 eqeltri 
 |-  Y e. _V
14 1 fvexi 
 |-  G e. _V
15 14 rnex 
 |-  ran G e. _V
16 3 15 eqeltri 
 |-  X e. _V
17 13 16 elmap 
 |-  ( F e. ( Y ^m X ) <-> F : X --> Y )
18 17 anbi1i 
 |-  ( ( F e. ( Y ^m X ) /\ ( ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) <-> ( F : X --> Y /\ ( ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) )
19 fveq1 
 |-  ( f = F -> ( f ` U ) = ( F ` U ) )
20 19 eqeq1d 
 |-  ( f = F -> ( ( f ` U ) = V <-> ( F ` U ) = V ) )
21 fveq1 
 |-  ( f = F -> ( f ` ( x G y ) ) = ( F ` ( x G y ) ) )
22 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
23 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
24 22 23 oveq12d 
 |-  ( f = F -> ( ( f ` x ) J ( f ` y ) ) = ( ( F ` x ) J ( F ` y ) ) )
25 21 24 eqeq12d 
 |-  ( f = F -> ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) <-> ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) ) )
26 fveq1 
 |-  ( f = F -> ( f ` ( x H y ) ) = ( F ` ( x H y ) ) )
27 22 23 oveq12d 
 |-  ( f = F -> ( ( f ` x ) K ( f ` y ) ) = ( ( F ` x ) K ( F ` y ) ) )
28 26 27 eqeq12d 
 |-  ( f = F -> ( ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) <-> ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) )
29 25 28 anbi12d 
 |-  ( f = F -> ( ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) <-> ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) )
30 29 2ralbidv 
 |-  ( f = F -> ( A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) <-> A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) )
31 20 30 anbi12d 
 |-  ( f = F -> ( ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) <-> ( ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) )
32 31 elrab 
 |-  ( F e. { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } <-> ( F e. ( Y ^m X ) /\ ( ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) )
33 3anass 
 |-  ( ( F : X --> Y /\ ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) <-> ( F : X --> Y /\ ( ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) )
34 18 32 33 3bitr4i 
 |-  ( F e. { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } <-> ( F : X --> Y /\ ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) )
35 10 34 bitrdi 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RngHom S ) <-> ( F : X --> Y /\ ( F ` U ) = V /\ A. x e. X A. y e. X ( ( F ` ( x G y ) ) = ( ( F ` x ) J ( F ` y ) ) /\ ( F ` ( x H y ) ) = ( ( F ` x ) K ( F ` y ) ) ) ) ) )