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 ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ) ∧ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ∧ 𝐺 ∈ ( 𝑆 RngHom 𝑇 ) ) ) → ( 𝐺𝐹 ) ∈ ( 𝑅 RngHom 𝑇 ) )

Proof

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