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 ) ) ) ) ) )