Theorem rnghomco 16128

Description: The composition of two ring homomorphisms is a ring homomorphism.

Assertion

Ref	Expression
rnghomco	|- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> (G o. F) e. (R RngHom T))

Proof of Theorem rnghomco

Step	Hyp	Ref	Expression
1		eqid 1884	. . . . . . . 8 |- (1st` S) = (1st` S)
2		eqid 1884	. . . . . . . 8 |- ran (1st` S) = ran (1st` S)
3		eqid 1884	. . . . . . . 8 |- (1st` T) = (1st` T)
4		eqid 1884	. . . . . . . 8 |- ran (1st` T) = ran (1st` T)
5	1, 2, 3, 4	rnghomf 16120	. . . . . . 7 |- ((S e. Ring /\ T e. Ring /\ G e. (S RngHom T)) -> G:ran (1st` S)-->ran (1st` T))
6	5	3expa 1067	. . . . . 6 |- (((S e. Ring /\ T e. Ring) /\ G e. (S RngHom T)) -> G:ran (1st` S)-->ran (1st` T))
7	6	3adantl1 1032	. . . . 5 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ G e. (S RngHom T)) -> G:ran (1st` S)-->ran (1st` T))
8	7	adantrl 430	. . . 4 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> G:ran (1st` S)-->ran (1st` T))
9		eqid 1884	. . . . . . . 8 |- (1st` R) = (1st` R)
10		eqid 1884	. . . . . . . 8 |- ran (1st` R) = ran (1st` R)
11	9, 10, 1, 2	rnghomf 16120	. . . . . . 7 |- ((R e. Ring /\ S e. Ring /\ F e. (R RngHom S)) -> F:ran (1st` R)-->ran (1st` S))
12	11	3expa 1067	. . . . . 6 |- (((R e. Ring /\ S e. Ring) /\ F e. (R RngHom S)) -> F:ran (1st` R)-->ran (1st` S))
13	12	3adantl3 1034	. . . . 5 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ F e. (R RngHom S)) -> F:ran (1st` R)-->ran (1st` S))
14	13	adantrr 431	. . . 4 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> F:ran (1st` R)-->ran (1st` S))
15		fco 4573	. . . 4 |- ((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	syl11anc 524	. . 3 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> (G o. F):ran (1st` R)-->ran (1st` T))
17		ffun 4565	. . . . . 6 |- (G:ran (1st` S)-->ran (1st` T) -> Fun G)
18	8, 17	syl 12	. . . . 5 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> Fun G)
19		eqid 1884	. . . . . . . 8 |- (2nd` R) = (2nd` R)
20		eqid 1884	. . . . . . . 8 |- (Id` (2nd` R)) = (Id` (2nd` R))
21	10, 19, 20	ring1cl 10415	. . . . . . 7 |- (R e. Ring -> (Id` (2nd` R)) e. ran (1st` R))
22	21	3ad2ant1 897	. . . . . 6 |- ((R e. Ring /\ S e. Ring /\ T e. Ring) -> (Id` (2nd` R)) e. ran (1st` R))
23	22	adantr 425	. . . . 5 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> (Id` (2nd` R)) e. ran (1st` R))
24		fvco3 4739	. . . . 5 |- ((Fun G /\ F:ran (1st` R)-->ran (1st` S) /\ (Id` (2nd` R)) e. ran (1st` R)) -> ((G o. F)` (Id` (2nd` R))) = (G` (F` (Id` (2nd` R)))))
25	18, 14, 23, 24	syl111anc 1100	. . . 4 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> ((G o. F)` (Id` (2nd` R))) = (G` (F` (Id` (2nd` R)))))
26		eqid 1884	. . . . . . . . 9 |- (2nd` S) = (2nd` S)
27		eqid 1884	. . . . . . . . 9 |- (Id` (2nd` S)) = (Id` (2nd` S))
28	19, 20, 26, 27	rnghom1 16122	. . . . . . . 8 |- ((R e. Ring /\ S e. Ring /\ F e. (R RngHom S)) -> (F` (Id` (2nd` R))) = (Id` (2nd` S)))
29	28	3expa 1067	. . . . . . 7 |- (((R e. Ring /\ S e. Ring) /\ F e. (R RngHom S)) -> (F` (Id` (2nd` R))) = (Id` (2nd` S)))
30	29	3adantl3 1034	. . . . . 6 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ F e. (R RngHom S)) -> (F` (Id` (2nd` R))) = (Id` (2nd` S)))
31	30	adantrr 431	. . . . 5 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> (F` (Id` (2nd` R))) = (Id` (2nd` S)))
32	31	fveq2d 4685	. . . 4 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> (G` (F` (Id` (2nd` R)))) = (G` (Id` (2nd` S))))
33		eqid 1884	. . . . . . . 8 |- (2nd` T) = (2nd` T)
34		eqid 1884	. . . . . . . 8 |- (Id` (2nd` T)) = (Id` (2nd` T))
35	26, 27, 33, 34	rnghom1 16122	. . . . . . 7 |- ((S e. Ring /\ T e. Ring /\ G e. (S RngHom T)) -> (G` (Id` (2nd` S))) = (Id` (2nd` T)))
36	35	3expa 1067	. . . . . 6 |- (((S e. Ring /\ T e. Ring) /\ G e. (S RngHom T)) -> (G` (Id` (2nd` S))) = (Id` (2nd` T)))
37	36	3adantl1 1032	. . . . 5 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ G e. (S RngHom T)) -> (G` (Id` (2nd` S))) = (Id` (2nd` T)))
38	37	adantrl 430	. . . 4 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> (G` (Id` (2nd` S))) = (Id` (2nd` T)))
39	25, 32, 38	3eqtrd 1929	. . 3 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> ((G o. F)` (Id` (2nd` R))) = (Id` (2nd` T)))
40	9, 10, 1	rnghomadd 16123	. . . . . . . . . . . . 13 |- (((R e. Ring /\ S e. Ring /\ F e. (R RngHom S)) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (F` (x(1st` R)y)) = ((F` x)(1st` S)(F` y)))
41	40	ex 402	. . . . . . . . . . . 12 |- ((R e. Ring /\ S e. Ring /\ F e. (R RngHom S)) -> ((x e. ran (1st` R) /\ y e. ran (1st` R)) -> (F` (x(1st` R)y)) = ((F` x)(1st` S)(F` y))))
42	41	3expa 1067	. . . . . . . . . . 11 |- (((R e. Ring /\ S e. Ring) /\ F e. (R RngHom S)) -> ((x e. ran (1st` R) /\ y e. ran (1st` R)) -> (F` (x(1st` R)y)) = ((F` x)(1st` S)(F` y))))
43	42	3adantl3 1034	. . . . . . . . . 10 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ F e. (R RngHom S)) -> ((x e. ran (1st` R) /\ y e. ran (1st` R)) -> (F` (x(1st` R)y)) = ((F` x)(1st` S)(F` y))))
44	43	imp 377	. . . . . . . . 9 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ F e. (R RngHom S)) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (F` (x(1st` R)y)) = ((F` x)(1st` S)(F` y)))
45	44	adantlrr 435	. . . . . . . 8 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (F` (x(1st` R)y)) = ((F` x)(1st` S)(F` y)))
46	45	fveq2d 4685	. . . . . . 7 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (G` (F` (x(1st` R)y))) = (G` ((F` x)(1st` S)(F` y))))
47	9, 10, 1, 2	rnghomcl 16121	. . . . . . . . . . . . . 14 |- (((R e. Ring /\ S e. Ring /\ F e. (R RngHom S)) /\ x e. ran (1st` R)) -> (F` x) e. ran (1st` S))
48	9, 10, 1, 2	rnghomcl 16121	. . . . . . . . . . . . . 14 |- (((R e. Ring /\ S e. Ring /\ F e. (R RngHom S)) /\ y e. ran (1st` R)) -> (F` y) e. ran (1st` S))
49	47, 48	anim12da 15647	. . . . . . . . . . . . 13 |- (((R e. Ring /\ S e. Ring /\ F e. (R RngHom 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	ex 402	. . . . . . . . . . . 12 |- ((R e. Ring /\ S e. Ring /\ F e. (R RngHom 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	3expa 1067	. . . . . . . . . . 11 |- (((R e. Ring /\ S e. Ring) /\ F e. (R RngHom 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	3adantl3 1034	. . . . . . . . . 10 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ F e. (R RngHom 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	imp 377	. . . . . . . . 9 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ F e. (R RngHom S)) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> ((F` x) e. ran (1st` S) /\ (F` y) e. ran (1st` S)))
54	53	adantlrr 435	. . . . . . . 8 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> ((F` x) e. ran (1st` S) /\ (F` y) e. ran (1st` S)))
55	1, 2, 3	rnghomadd 16123	. . . . . . . . . . . . 13 |- (((S e. Ring /\ T e. Ring /\ G e. (S RngHom 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	ex 402	. . . . . . . . . . . 12 |- ((S e. Ring /\ T e. Ring /\ G e. (S RngHom 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	3expa 1067	. . . . . . . . . . 11 |- (((S e. Ring /\ T e. Ring) /\ G e. (S RngHom 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	3adantl1 1032	. . . . . . . . . 10 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ G e. (S RngHom 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	imp 377	. . . . . . . . 9 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ G e. (S RngHom 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	59	adantlrl 434	. . . . . . . 8 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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))))
61	54, 60	syldan 516	. . . . . . 7 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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))))
62	46, 61	eqtrd 1925	. . . . . 6 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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))))
63	9, 10	ringgcl 9477	. . . . . . . . . 10 |- ((R e. Ring /\ x e. ran (1st` R) /\ y e. ran (1st` R)) -> (x(1st` R)y) e. ran (1st` R))
64	63	3expb 1068	. . . . . . . . 9 |- ((R e. Ring /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (x(1st` R)y) e. ran (1st` R))
65	64	3ad2antl1 1038	. . . . . . . 8 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (x(1st` R)y) e. ran (1st` R))
66	65	adantlr 429	. . . . . . 7 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (x(1st` R)y) e. ran (1st` R))
67		fvco3 4739	. . . . . . . . 9 |- ((Fun G /\ 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))))
68	67	3expa 1067	. . . . . . . 8 |- (((Fun G /\ 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))))
69	18, 14	jca 310	. . . . . . . 8 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> (Fun G /\ F:ran (1st` R)-->ran (1st` S)))
70	68, 69	sylan 497	. . . . . . 7 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ (x(1st` R)y) e. ran (1st` R)) -> ((G o. F)` (x(1st` R)y)) = (G` (F` (x(1st` R)y))))
71	66, 70	syldan 516	. . . . . 6 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> ((G o. F)` (x(1st` R)y)) = (G` (F` (x(1st` R)y))))
72		fvco3 4739	. . . . . . . . . 10 |- ((Fun G /\ F:ran (1st` R)-->ran (1st` S) /\ x e. ran (1st` R)) -> ((G o. F)` x) = (G` (F` x)))
73	72	3expa 1067	. . . . . . . . 9 |- (((Fun G /\ F:ran (1st` R)-->ran (1st` S)) /\ x e. ran (1st` R)) -> ((G o. F)` x) = (G` (F` x)))
74	73, 69	sylan 497	. . . . . . . 8 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ x e. ran (1st` R)) -> ((G o. F)` x) = (G` (F` x)))
75		fvco3 4739	. . . . . . . . . 10 |- ((Fun G /\ F:ran (1st` R)-->ran (1st` S) /\ y e. ran (1st` R)) -> ((G o. F)` y) = (G` (F` y)))
76	75	3expa 1067	. . . . . . . . 9 |- (((Fun G /\ F:ran (1st` R)-->ran (1st` S)) /\ y e. ran (1st` R)) -> ((G o. F)` y) = (G` (F` y)))
77	76, 69	sylan 497	. . . . . . . 8 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ y e. ran (1st` R)) -> ((G o. F)` y) = (G` (F` y)))
78	74, 77	anim12da 15647	. . . . . . 7 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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))))
79		opreq12 4891	. . . . . . 7 |- ((((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))))
80	78, 79	syl 12	. . . . . 6 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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))))
81	62, 71, 80	3eqtr4d 1937	. . . . 5 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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)))
82	9, 10, 19, 26	rnghommul 16124	. . . . . . . . . . . . 13 |- (((R e. Ring /\ S e. Ring /\ F e. (R RngHom S)) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (F` (x(2nd` R)y)) = ((F` x)(2nd` S)(F` y)))
83	82	ex 402	. . . . . . . . . . . 12 |- ((R e. Ring /\ S e. Ring /\ F e. (R RngHom S)) -> ((x e. ran (1st` R) /\ y e. ran (1st` R)) -> (F` (x(2nd` R)y)) = ((F` x)(2nd` S)(F` y))))
84	83	3expa 1067	. . . . . . . . . . 11 |- (((R e. Ring /\ S e. Ring) /\ F e. (R RngHom S)) -> ((x e. ran (1st` R) /\ y e. ran (1st` R)) -> (F` (x(2nd` R)y)) = ((F` x)(2nd` S)(F` y))))
85	84	3adantl3 1034	. . . . . . . . . 10 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ F e. (R RngHom S)) -> ((x e. ran (1st` R) /\ y e. ran (1st` R)) -> (F` (x(2nd` R)y)) = ((F` x)(2nd` S)(F` y))))
86	85	imp 377	. . . . . . . . 9 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ F e. (R RngHom S)) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (F` (x(2nd` R)y)) = ((F` x)(2nd` S)(F` y)))
87	86	adantlrr 435	. . . . . . . 8 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (F` (x(2nd` R)y)) = ((F` x)(2nd` S)(F` y)))
88	87	fveq2d 4685	. . . . . . 7 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (G` (F` (x(2nd` R)y))) = (G` ((F` x)(2nd` S)(F` y))))
89	1, 2, 26, 33	rnghommul 16124	. . . . . . . . . . . . 13 |- (((S e. Ring /\ T e. Ring /\ G e. (S RngHom 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	89	ex 402	. . . . . . . . . . . 12 |- ((S e. Ring /\ T e. Ring /\ G e. (S RngHom 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)))))
91	90	3expa 1067	. . . . . . . . . . 11 |- (((S e. Ring /\ T e. Ring) /\ G e. (S RngHom 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)))))
92	91	3adantl1 1032	. . . . . . . . . 10 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ G e. (S RngHom 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)))))
93	92	imp 377	. . . . . . . . 9 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ G e. (S RngHom 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))))
94	93	adantlrl 434	. . . . . . . 8 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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))))
95	54, 94	syldan 516	. . . . . . 7 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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))))
96	88, 95	eqtrd 1925	. . . . . 6 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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))))
97	9, 19, 10	ringcl 9468	. . . . . . . . . 10 |- ((R e. Ring /\ x e. ran (1st` R) /\ y e. ran (1st` R)) -> (x(2nd` R)y) e. ran (1st` R))
98	97	3expb 1068	. . . . . . . . 9 |- ((R e. Ring /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (x(2nd` R)y) e. ran (1st` R))
99	98	3ad2antl1 1038	. . . . . . . 8 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (x(2nd` R)y) e. ran (1st` R))
100	99	adantlr 429	. . . . . . 7 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> (x(2nd` R)y) e. ran (1st` R))
101		fvco3 4739	. . . . . . . . 9 |- ((Fun G /\ 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))))
102	101	3expa 1067	. . . . . . . 8 |- (((Fun G /\ 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))))
103	102, 69	sylan 497	. . . . . . 7 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ (x(2nd` R)y) e. ran (1st` R)) -> ((G o. F)` (x(2nd` R)y)) = (G` (F` (x(2nd` R)y))))
104	100, 103	syldan 516	. . . . . 6 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) /\ (x e. ran (1st` R) /\ y e. ran (1st` R))) -> ((G o. F)` (x(2nd` R)y)) = (G` (F` (x(2nd` R)y))))
105		opreq12 4891	. . . . . . 7 |- ((((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))))
106	78, 105	syl 12	. . . . . 6 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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))))
107	96, 104, 106	3eqtr4d 1937	. . . . 5 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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)))
108	81, 107	jca 310	. . . 4 |- ((((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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))))
109	108	r19.21aivva 15653	. . 3 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom 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))))
110	16, 39, 109	3jca 1050	. 2 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> ((G o. F):ran (1st` R)-->ran (1st` T) /\ ((G o. F)` (Id` (2nd` R))) = (Id` (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)))))
111	9, 19, 10, 20, 3, 33, 4, 34	isrnghom 16119	. . . 4 |- ((R e. Ring /\ T e. Ring) -> ((G o. F) e. (R RngHom T) <-> ((G o. F):ran (1st` R)-->ran (1st` T) /\ ((G o. F)` (Id` (2nd` R))) = (Id` (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))))))
112	111	3adant2 895	. . 3 |- ((R e. Ring /\ S e. Ring /\ T e. Ring) -> ((G o. F) e. (R RngHom T) <-> ((G o. F):ran (1st` R)-->ran (1st` T) /\ ((G o. F)` (Id` (2nd` R))) = (Id` (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))))))
113	112	adantr 425	. 2 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> ((G o. F) e. (R RngHom T) <-> ((G o. F):ran (1st` R)-->ran (1st` T) /\ ((G o. F)` (Id` (2nd` R))) = (Id` (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))))))
114	110, 113	mpbird 213	1 |- (((R e. Ring /\ S e. Ring /\ T e. Ring) /\ (F e. (R RngHom S) /\ G e. (S RngHom T))) -> (G o. F) e. (R RngHom T))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  ran crn 3987   o. ccom 3990  Fun wfun 3992  -->wf 3994  ` cfv 3998  (class class class)co 4884  1stc1st 5018  2ndc2nd 5019  Idcgi 9312  Ringcring 9463   RngHom crnghom 16114

This theorem is referenced by:  rngisoco 16136

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fo 4012  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-2nd 5021  df-grp 9316  df-gid 9317  df-abl 9408  df-ring 9464  df-ass 10360  df-exid 10362  df-mgm 10366  df-sgr 10378  df-mnd 10385  df-rnghom 16117

Copyright terms: Public domain