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 32175

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 2423	. . . . . . 7
2		eqid 2423	. . . . . . 7
3		eqid 2423	. . . . . . 7
4		eqid 2423	. . . . . . 7
5	1, 2, 3, 4	rngohomf 32167	. . . . . 6 $/\$ $/\$
6	5	3expa 1206	. . . . 5 $/\$ $/\$
7	6	3adantl1 1162	. . . 4 $/\$ $/\$ $/\$
8	7	adantrl 721	. . 3 $/\$ $/\$ $/\$ $/\$
9		eqid 2423	. . . . . . 7
10		eqid 2423	. . . . . . 7
11	9, 10, 1, 2	rngohomf 32167	. . . . . 6 $/\$ $/\$
12	11	3expa 1206	. . . . 5 $/\$ $/\$
13	12	3adantl3 1164	. . . 4 $/\$ $/\$ $/\$
14	13	adantrr 722	. . 3 $/\$ $/\$ $/\$ $/\$
15		fco 5755	. . 3 $/\$
16	8, 14, 15	syl2anc 666	. 2 $/\$ $/\$ $/\$ $/\$
17		eqid 2423	. . . . . . 7
18		eqid 2423	. . . . . . 7 GId GId
19	10, 17, 18	rngo1cl 26153	. . . . . 6 GId
20	19	3ad2ant1 1027	. . . . 5 $/\$ $/\$ GId
21	20	adantr 467	. . . 4 $/\$ $/\$ $/\$ $/\$ GId
22		fvco3 5957	. . . 4 $/\$ GId GId GId
23	14, 21, 22	syl2anc 666	. . 3 $/\$ $/\$ $/\$ $/\$ GId GId
24		eqid 2423	. . . . . . . . 9
25		eqid 2423	. . . . . . . . 9 GId GId
26	17, 18, 24, 25	rngohom1 32169	. . . . . . . 8 $/\$ $/\$ GId GId
27	26	3expa 1206	. . . . . . 7 $/\$ $/\$ GId GId
28	27	3adantl3 1164	. . . . . 6 $/\$ $/\$ $/\$ GId GId
29	28	adantrr 722	. . . . 5 $/\$ $/\$ $/\$ $/\$ GId GId
30	29	fveq2d 5884	. . . 4 $/\$ $/\$ $/\$ $/\$ GId GId
31		eqid 2423	. . . . . . . 8
32		eqid 2423	. . . . . . . 8 GId GId
33	24, 25, 31, 32	rngohom1 32169	. . . . . . 7 $/\$ $/\$ GId GId
34	33	3expa 1206	. . . . . 6 $/\$ $/\$ GId GId
35	34	3adantl1 1162	. . . . 5 $/\$ $/\$ $/\$ GId GId
36	35	adantrl 721	. . . 4 $/\$ $/\$ $/\$ $/\$ GId GId
37	30, 36	eqtrd 2464	. . 3 $/\$ $/\$ $/\$ $/\$ GId GId
38	23, 37	eqtrd 2464	. 2 $/\$ $/\$ $/\$ $/\$ GId GId
39	9, 10, 1	rngohomadd 32170	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
40	39	ex 436	. . . . . . . . . . 11 $/\$ $/\$ $/\$
41	40	3expa 1206	. . . . . . . . . 10 $/\$ $/\$ $/\$
42	41	3adantl3 1164	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
43	42	imp 431	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
44	43	adantlrr 726	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	44	fveq2d 5884	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	9, 10, 1, 2	rngohomcl 32168	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
47	9, 10, 1, 2	rngohomcl 32168	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
48	46, 47	anim12da 32000	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
49	48	ex 436	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
50	49	3expa 1206	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
51	50	3adantl3 1164	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
52	51	imp 431	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	52	adantlrr 726	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	1, 2, 3	rngohomadd 32170	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
55	54	ex 436	. . . . . . . . . . 11 $/\$ $/\$ $/\$
56	55	3expa 1206	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	3adantl1 1162	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
58	57	imp 431	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
59	58	adantlrl 725	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	53, 59	syldan 473	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	45, 60	eqtrd 2464	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62	9, 10	rngogcl 26115	. . . . . . . . 9 $/\$ $/\$
63	62	3expb 1207	. . . . . . . 8 $/\$ $/\$
64	63	3ad2antl1 1168	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
65	64	adantlr 720	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66		fvco3 5957	. . . . . . 7 $/\$
67	14, 66	sylan 474	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
68	65, 67	syldan 473	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		fvco3 5957	. . . . . . . 8 $/\$
70	14, 69	sylan 474	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
71		fvco3 5957	. . . . . . . 8 $/\$
72	14, 71	sylan 474	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
73	70, 72	anim12da 32000	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74		oveq12 6313	. . . . . 6 $/\$
75	73, 74	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76	61, 68, 75	3eqtr4d 2474	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77	9, 10, 17, 24	rngohommul 32171	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
78	77	ex 436	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	78	3expa 1206	. . . . . . . . . 10 $/\$ $/\$ $/\$
80	79	3adantl3 1164	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
81	80	imp 431	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
82	81	adantlrr 726	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	82	fveq2d 5884	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84	1, 2, 24, 31	rngohommul 32171	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
85	84	ex 436	. . . . . . . . . . 11 $/\$ $/\$ $/\$
86	85	3expa 1206	. . . . . . . . . 10 $/\$ $/\$ $/\$
87	86	3adantl1 1162	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
88	87	imp 431	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
89	88	adantlrl 725	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90	53, 89	syldan 473	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	83, 90	eqtrd 2464	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
92	9, 17, 10	rngocl 26106	. . . . . . . . 9 $/\$ $/\$
93	92	3expb 1207	. . . . . . . 8 $/\$ $/\$
94	93	3ad2antl1 1168	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
95	94	adantlr 720	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		fvco3 5957	. . . . . . 7 $/\$
97	14, 96	sylan 474	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
98	95, 97	syldan 473	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		oveq12 6313	. . . . . 6 $/\$
100	73, 99	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	91, 98, 100	3eqtr4d 2474	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	76, 101	jca 535	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	102	ralrimivva 2847	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
104	9, 17, 10, 18, 3, 31, 4, 32	isrngohom 32166	. . . 4 $/\$ $/\$ GId GId $/\$ $/\$
105	104	3adant2 1025	. . 3 $/\$ $/\$ $/\$ GId GId $/\$ $/\$
106	105	adantr 467	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ GId GId $/\$ $/\$
107	16, 38, 103, 106	mpbir3and 1189	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 983

wceq 1438

wcel 1869

wral 2776

crn 4853

ccom 4856

wf 5596

cfv 5600 (class class class)co 6304

c1st 6804

c2nd 6805 GIdcgi 25911

crngo 26099

crnghom 32161

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-sep 4545 ax-nul 4554 ax-pow 4601 ax-pr 4659 ax-un 6596

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3302 df-csb 3398 df-dif 3441 df-un 3443 df-in 3445 df-ss 3452 df-nul 3764 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-op 4005 df-uni 4219 df-iun 4300 df-br 4423 df-opab 4482 df-mpt 4483 df-id 4767 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-fo 5606 df-fv 5608 df-riota 6266 df-ov 6307 df-oprab 6308 df-mpt2 6309 df-1st 6806 df-2nd 6807 df-map 7484 df-grpo 25915 df-gid 25916 df-ablo 26006 df-ass 26037 df-exid 26039 df-mgmOLD 26043 df-sgrOLD 26055 df-mndo 26062 df-rngo 26100 df-rngohom 32164

This theorem is referenced by: rngoisoco 32183

W3C validator