rngohomco - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > rngohomco		Structured version Unicode version

Theorem rngohomco 28920

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

**Assertion**
Ref	Expression
rngohomco	$/\$ $/\$ $/\$ $/\$

Proof of Theorem rngohomco Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2451	. . . . . . 7
2		eqid 2451	. . . . . . 7
3		eqid 2451	. . . . . . 7
4		eqid 2451	. . . . . . 7
5	1, 2, 3, 4	rngohomf 28912	. . . . . 6 $/\$ $/\$
6	5	3expa 1188	. . . . 5 $/\$ $/\$
7	6	3adantl1 1144	. . . 4 $/\$ $/\$ $/\$
8	7	adantrl 715	. . 3 $/\$ $/\$ $/\$ $/\$
9		eqid 2451	. . . . . . 7
10		eqid 2451	. . . . . . 7
11	9, 10, 1, 2	rngohomf 28912	. . . . . 6 $/\$ $/\$
12	11	3expa 1188	. . . . 5 $/\$ $/\$
13	12	3adantl3 1146	. . . 4 $/\$ $/\$ $/\$
14	13	adantrr 716	. . 3 $/\$ $/\$ $/\$ $/\$
15		fco 5668	. . 3 $/\$
16	8, 14, 15	syl2anc 661	. 2 $/\$ $/\$ $/\$ $/\$
17		eqid 2451	. . . . . . 7
18		eqid 2451	. . . . . . 7 GId GId
19	10, 17, 18	rngo1cl 24053	. . . . . 6 GId
20	19	3ad2ant1 1009	. . . . 5 $/\$ $/\$ GId
21	20	adantr 465	. . . 4 $/\$ $/\$ $/\$ $/\$ GId
22		fvco3 5869	. . . 4 $/\$ GId GId GId
23	14, 21, 22	syl2anc 661	. . 3 $/\$ $/\$ $/\$ $/\$ GId GId
24		eqid 2451	. . . . . . . . 9
25		eqid 2451	. . . . . . . . 9 GId GId
26	17, 18, 24, 25	rngohom1 28914	. . . . . . . 8 $/\$ $/\$ GId GId
27	26	3expa 1188	. . . . . . 7 $/\$ $/\$ GId GId
28	27	3adantl3 1146	. . . . . 6 $/\$ $/\$ $/\$ GId GId
29	28	adantrr 716	. . . . 5 $/\$ $/\$ $/\$ $/\$ GId GId
30	29	fveq2d 5795	. . . 4 $/\$ $/\$ $/\$ $/\$ GId GId
31		eqid 2451	. . . . . . . 8
32		eqid 2451	. . . . . . . 8 GId GId
33	24, 25, 31, 32	rngohom1 28914	. . . . . . 7 $/\$ $/\$ GId GId
34	33	3expa 1188	. . . . . 6 $/\$ $/\$ GId GId
35	34	3adantl1 1144	. . . . 5 $/\$ $/\$ $/\$ GId GId
36	35	adantrl 715	. . . 4 $/\$ $/\$ $/\$ $/\$ GId GId
37	30, 36	eqtrd 2492	. . 3 $/\$ $/\$ $/\$ $/\$ GId GId
38	23, 37	eqtrd 2492	. 2 $/\$ $/\$ $/\$ $/\$ GId GId
39	9, 10, 1	rngohomadd 28915	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
40	39	ex 434	. . . . . . . . . . 11 $/\$ $/\$ $/\$
41	40	3expa 1188	. . . . . . . . . 10 $/\$ $/\$ $/\$
42	41	3adantl3 1146	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
43	42	imp 429	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
44	43	adantlrr 720	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	44	fveq2d 5795	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	9, 10, 1, 2	rngohomcl 28913	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
47	9, 10, 1, 2	rngohomcl 28913	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
48	46, 47	anim12da 28744	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
49	48	ex 434	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
50	49	3expa 1188	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
51	50	3adantl3 1146	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
52	51	imp 429	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	52	adantlrr 720	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	1, 2, 3	rngohomadd 28915	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
55	54	ex 434	. . . . . . . . . . 11 $/\$ $/\$ $/\$
56	55	3expa 1188	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	3adantl1 1144	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
58	57	imp 429	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
59	58	adantlrl 719	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	53, 59	syldan 470	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	45, 60	eqtrd 2492	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	9, 10	rngogcl 24015	. . . . . . . . 9 $/\$ $/\$
63	62	3expb 1189	. . . . . . . 8 $/\$ $/\$
64	63	3ad2antl1 1150	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
65	64	adantlr 714	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66		fvco3 5869	. . . . . . 7 $/\$
67	14, 66	sylan 471	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
68	65, 67	syldan 470	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		fvco3 5869	. . . . . . . 8 $/\$
70	14, 69	sylan 471	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
71		fvco3 5869	. . . . . . . 8 $/\$
72	14, 71	sylan 471	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
73	70, 72	anim12da 28744	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74		oveq12 6201	. . . . . 6 $/\$
75	73, 74	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76	61, 68, 75	3eqtr4d 2502	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	9, 10, 17, 24	rngohommul 28916	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
78	77	ex 434	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	78	3expa 1188	. . . . . . . . . 10 $/\$ $/\$ $/\$
80	79	3adantl3 1146	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
81	80	imp 429	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
82	81	adantlrr 720	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	82	fveq2d 5795	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84	1, 2, 24, 31	rngohommul 28916	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
85	84	ex 434	. . . . . . . . . . 11 $/\$ $/\$ $/\$
86	85	3expa 1188	. . . . . . . . . 10 $/\$ $/\$ $/\$
87	86	3adantl1 1144	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
88	87	imp 429	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
89	88	adantlrl 719	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90	53, 89	syldan 470	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	83, 90	eqtrd 2492	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	9, 17, 10	rngocl 24006	. . . . . . . . 9 $/\$ $/\$
93	92	3expb 1189	. . . . . . . 8 $/\$ $/\$
94	93	3ad2antl1 1150	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
95	94	adantlr 714	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		fvco3 5869	. . . . . . 7 $/\$
97	14, 96	sylan 471	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
98	95, 97	syldan 470	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		oveq12 6201	. . . . . 6 $/\$
100	73, 99	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	91, 98, 100	3eqtr4d 2502	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	76, 101	jca 532	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	102	ralrimivva 2906	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
104	9, 17, 10, 18, 3, 31, 4, 32	isrngohom 28911	. . . 4 $/\$ $/\$ GId GId $/\$ $/\$
105	104	3adant2 1007	. . 3 $/\$ $/\$ $/\$ GId GId $/\$ $/\$
106	105	adantr 465	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ GId GId $/\$ $/\$
107	16, 38, 103, 106	mpbir3and 1171	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758

wral 2795

crn 4941

ccom 4944

wf 5514

cfv 5518 (class class class)co 6192

c1st 6677

c2nd 6678 GIdcgi 23811

crngo 23999

crnghom 28906

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4513 ax-nul 4521 ax-pow 4570 ax-pr 4631 ax-un 6474

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3072 df-sbc 3287 df-csb 3389 df-dif 3431 df-un 3433 df-in 3435 df-ss 3442 df-nul 3738 df-if 3892 df-pw 3962 df-sn 3978 df-pr 3980 df-op 3984 df-uni 4192 df-iun 4273 df-br 4393 df-opab 4451 df-mpt 4452 df-id 4736 df-xp 4946 df-rel 4947 df-cnv 4948 df-co 4949 df-dm 4950 df-rn 4951 df-res 4952 df-ima 4953 df-iota 5481 df-fun 5520 df-fn 5521 df-f 5522 df-fo 5524 df-fv 5526 df-riota 6153 df-ov 6195 df-oprab 6196 df-mpt2 6197 df-1st 6679 df-2nd 6680 df-map 7318 df-grpo 23815 df-gid 23816 df-ablo 23906 df-ass 23937 df-exid 23939 df-mgm 23943 df-sgr 23955 df-mndo 23962 df-rngo 24000 df-rngohom 28909

This theorem is referenced by: rngoisoco 28928

W3C validator