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

Metamath Proof Explorer

Theorem rngohomco

Proof