Metamath Proof Explorer

Theorem rngohomco

Description: The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Assertion rngohomco 
|- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G o. F ) e. ( R RingOpsHom T ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 1st ` S ) = ( 1st ` S )
2 eqid 
 |-  ran ( 1st ` S ) = ran ( 1st ` S )
3 eqid 
 |-  ( 1st ` T ) = ( 1st ` T )
4 eqid 
 |-  ran ( 1st ` T ) = ran ( 1st ` T )
5 1 2 3 4 rngohomf 
 |-  ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) )
6 5 3expa 
 |-  ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) )
7 6 3adantl1 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) )
8 7 adantrl 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> G : ran ( 1st ` S ) --> ran ( 1st ` T ) )
9 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
10 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
11 9 10 1 2 rngohomf 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) )
12 11 3expa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) )
13 12 3adantl3 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) )
14 13 adantrr 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> F : ran ( 1st ` R ) --> ran ( 1st ` S ) )
15 fco 
 |-  ( ( G : ran ( 1st ` S ) --> ran ( 1st ` T ) /\ F : ran ( 1st ` R ) --> ran ( 1st ` S ) ) -> ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) )
16 8 14 15 syl2anc 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) )
17 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
18 eqid 
 |-  ( GId ` ( 2nd ` R ) ) = ( GId ` ( 2nd ` R ) )
19 10 17 18 rngo1cl 
 |-  ( R e. RingOps -> ( GId ` ( 2nd ` R ) ) e. ran ( 1st ` R ) )
20 19 3ad2ant1 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) -> ( GId ` ( 2nd ` R ) ) e. ran ( 1st ` R ) )
21 20 adantr 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( GId ` ( 2nd ` R ) ) e. ran ( 1st ` R ) )
22 fvco3 
 |-  ( ( F : ran ( 1st ` R ) --> ran ( 1st ` S ) /\ ( GId ` ( 2nd ` R ) ) e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( G ` ( F ` ( GId ` ( 2nd ` R ) ) ) ) )
23 14 21 22 syl2anc 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( G ` ( F ` ( GId ` ( 2nd ` R ) ) ) ) )
24 eqid 
 |-  ( 2nd ` S ) = ( 2nd ` S )
25 eqid 
 |-  ( GId ` ( 2nd ` S ) ) = ( GId ` ( 2nd ` S ) )
26 17 18 24 25 rngohom1 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) )
27 26 3expa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) )
28 27 3adantl3 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) )
29 28 adantrr 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) )
30 29 fveq2d 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G ` ( F ` ( GId ` ( 2nd ` R ) ) ) ) = ( G ` ( GId ` ( 2nd ` S ) ) ) )
31 eqid 
 |-  ( 2nd ` T ) = ( 2nd ` T )
32 eqid 
 |-  ( GId ` ( 2nd ` T ) ) = ( GId ` ( 2nd ` T ) )
33 24 25 31 32 rngohom1 
 |-  ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) )
34 33 3expa 
 |-  ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) )
35 34 3adantl1 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) )
36 35 adantrl 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` T ) ) )
37 30 36 eqtrd 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G ` ( F ` ( GId ` ( 2nd ` R ) ) ) ) = ( GId ` ( 2nd ` T ) ) )
38 23 37 eqtrd 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) )
39 9 10 1 rngohomadd 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) )
40 39 ex 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) )
41 40 3expa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) )
42 41 3adantl3 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) )
43 42 imp 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) )
44 43 adantlrr 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 1st ` R ) y ) ) = ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) )
45 44 fveq2d 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) = ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) )
46 9 10 1 2 rngohomcl 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ x e. ran ( 1st ` R ) ) -> ( F ` x ) e. ran ( 1st ` S ) )
47 9 10 1 2 rngohomcl 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ y e. ran ( 1st ` R ) ) -> ( F ` y ) e. ran ( 1st ` S ) )
48 46 47 anim12dan 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) )
49 48 ex 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) )
50 49 3expa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) )
51 50 3adantl3 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) )
52 51 imp 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) )
53 52 adantlrr 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) )
54 1 2 3 rngohomadd 
 |-  ( ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) )
55 54 ex 
 |-  ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) )
56 55 3expa 
 |-  ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) )
57 56 3adantl1 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) ) )
58 57 imp 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) )
59 58 adantlrl 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) )
60 53 59 syldan 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( ( F ` x ) ( 1st ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) )
61 45 60 eqtrd 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) )
62 9 10 rngogcl 
 |-  ( ( R e. RingOps /\ x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( x ( 1st ` R ) y ) e. ran ( 1st ` R ) )
63 62 3expb 
 |-  ( ( R e. RingOps /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( x ( 1st ` R ) y ) e. ran ( 1st ` R ) )
64 63 3ad2antl1 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( x ( 1st ` R ) y ) e. ran ( 1st ` R ) )
65 64 adantlr 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( x ( 1st ` R ) y ) e. ran ( 1st ` R ) )
66 fvco3 
 |-  ( ( F : ran ( 1st ` R ) --> ran ( 1st ` S ) /\ ( x ( 1st ` R ) y ) e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) )
67 14 66 sylan 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x ( 1st ` R ) y ) e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) )
68 65 67 syldan 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( G ` ( F ` ( x ( 1st ` R ) y ) ) ) )
69 fvco3 
 |-  ( ( F : ran ( 1st ` R ) --> ran ( 1st ` S ) /\ x e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
70 14 69 sylan 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ x e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
71 fvco3 
 |-  ( ( F : ran ( 1st ` R ) --> ran ( 1st ` S ) /\ y e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` y ) = ( G ` ( F ` y ) ) )
72 14 71 sylan 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ y e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` y ) = ( G ` ( F ` y ) ) )
73 70 72 anim12dan 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) /\ ( ( G o. F ) ` y ) = ( G ` ( F ` y ) ) ) )
74 oveq12 
 |-  ( ( ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) /\ ( ( G o. F ) ` y ) = ( G ` ( F ` y ) ) ) -> ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) )
75 73 74 syl 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) = ( ( G ` ( F ` x ) ) ( 1st ` T ) ( G ` ( F ` y ) ) ) )
76 61 68 75 3eqtr4d 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) )
77 9 10 17 24 rngohommul 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) )
78 77 ex 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) )
79 78 3expa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) )
80 79 3adantl3 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) )
81 80 imp 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsHom S ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) )
82 81 adantlrr 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( F ` ( x ( 2nd ` R ) y ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) )
83 82 fveq2d 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) = ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) )
84 1 2 24 31 rngohommul 
 |-  ( ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) )
85 84 ex 
 |-  ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) )
86 85 3expa 
 |-  ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) )
87 86 3adantl1 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) -> ( ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) ) )
88 87 imp 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsHom T ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) )
89 88 adantlrl 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( ( F ` x ) e. ran ( 1st ` S ) /\ ( F ` y ) e. ran ( 1st ` S ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) )
90 53 89 syldan 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( ( F ` x ) ( 2nd ` S ) ( F ` y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) )
91 83 90 eqtrd 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) )
92 9 17 10 rngocl 
 |-  ( ( R e. RingOps /\ x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) -> ( x ( 2nd ` R ) y ) e. ran ( 1st ` R ) )
93 92 3expb 
 |-  ( ( R e. RingOps /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( x ( 2nd ` R ) y ) e. ran ( 1st ` R ) )
94 93 3ad2antl1 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( x ( 2nd ` R ) y ) e. ran ( 1st ` R ) )
95 94 adantlr 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( x ( 2nd ` R ) y ) e. ran ( 1st ` R ) )
96 fvco3 
 |-  ( ( F : ran ( 1st ` R ) --> ran ( 1st ` S ) /\ ( x ( 2nd ` R ) y ) e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) )
97 14 96 sylan 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x ( 2nd ` R ) y ) e. ran ( 1st ` R ) ) -> ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) )
98 95 97 syldan 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( G ` ( F ` ( x ( 2nd ` R ) y ) ) ) )
99 oveq12 
 |-  ( ( ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) /\ ( ( G o. F ) ` y ) = ( G ` ( F ` y ) ) ) -> ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) )
100 73 99 syl 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) = ( ( G ` ( F ` x ) ) ( 2nd ` T ) ( G ` ( F ` y ) ) ) )
101 91 98 100 3eqtr4d 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) )
102 76 101 jca 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) ) ) -> ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) )
103 102 ralrimivva 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) )
104 9 17 10 18 3 31 4 32 isrngohom 
 |-  ( ( R e. RingOps /\ T e. RingOps ) -> ( ( G o. F ) e. ( R RingOpsHom T ) <-> ( ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) /\ ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) ) )
105 104 3adant2 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) -> ( ( G o. F ) e. ( R RingOpsHom T ) <-> ( ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) /\ ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) ) )
106 105 adantr 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( ( G o. F ) e. ( R RingOpsHom T ) <-> ( ( G o. F ) : ran ( 1st ` R ) --> ran ( 1st ` T ) /\ ( ( G o. F ) ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` T ) ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( ( G o. F ) ` ( x ( 1st ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 1st ` T ) ( ( G o. F ) ` y ) ) /\ ( ( G o. F ) ` ( x ( 2nd ` R ) y ) ) = ( ( ( G o. F ) ` x ) ( 2nd ` T ) ( ( G o. F ) ` y ) ) ) ) ) )
107 16 38 103 106 mpbir3and 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G o. F ) e. ( R RingOpsHom T ) )