rngohomco

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

		Ref	Expression
	Assertion	rngohomco	$⊢ ((R \in RingOps \land S \in RingOps \land T \in RingOps) \land (F \in (R RngHom S) \land G \in (S RngHom T))) \to G \circ F \in (R RngHom T)$

Proof

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

Metamath Proof Explorer

Theorem rngohomco

Proof