rngisocnv - Mathbox for Jeff Madsen

Mathbox for Jeff Madsen

< Previous Next >
Related theorems
Unicode version

Theorem rngisocnv 16135

Description: The inverse of a ring isomorphism is a ring isomorphism.

**Assertion**
Ref	Expression
rngisocnv	Ring $/\$ Ring $/\$ RngIso RngIso

**Proof of Theorem rngisocnv**
Step	Hyp	Ref	Expression
1		f1ocnv 4651	. . . . . . . . 9
2		f1of 4635	. . . . . . . . 9
3	1, 2	syl 12	. . . . . . . 8
4	3	ad2antll 443	. . . . . . 7 Ring $/\$ Ring $/\$ RngHom $/\$
5		eqid 1884	. . . . . . . . . . 11
6		eqid 1884	. . . . . . . . . . 11 Id Id
7		eqid 1884	. . . . . . . . . . 11
8		eqid 1884	. . . . . . . . . . 11 Id Id
9	5, 6, 7, 8	rnghom1 16122	. . . . . . . . . 10 Ring $/\$ Ring $/\$ RngHom Id Id
10	9	3expa 1067	. . . . . . . . 9 Ring $/\$ Ring $/\$ RngHom Id Id
11	10	adantrr 431	. . . . . . . 8 Ring $/\$ Ring $/\$ RngHom $/\$ Id Id
12		f1ocnvfv 4856	. . . . . . . . . . 11 $/\$ Id Id Id Id Id
13		eqid 1884	. . . . . . . . . . . 12
14	13, 5, 6	ring1cl 10415	. . . . . . . . . . 11 Ring Id
15	12, 14	sylan2 500	. . . . . . . . . 10 $/\$ Ring Id Id Id Id
16	15	ancoms 484	. . . . . . . . 9 Ring $/\$ Id Id Id Id
17	16	ad2ant2rl 447	. . . . . . . 8 Ring $/\$ Ring $/\$ RngHom $/\$ Id Id Id Id
18	11, 17	mpd 29	. . . . . . 7 Ring $/\$ Ring $/\$ RngHom $/\$ Id Id
19		f1ocnvfv2 4855	. . . . . . . . . . . . . . 15 $/\$
20		f1ocnvfv2 4855	. . . . . . . . . . . . . . 15 $/\$
21	19, 20	anim12da 15647	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
22		opreq12 4891	. . . . . . . . . . . . . 14 $/\$
23	21, 22	syl 12	. . . . . . . . . . . . 13 $/\$ $/\$
24	23	adantll 428	. . . . . . . . . . . 12 RngHom $/\$ $/\$ $/\$
25	24	adantll 428	. . . . . . . . . . 11 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
26		eqid 1884	. . . . . . . . . . . . . . . . 17
27		eqid 1884	. . . . . . . . . . . . . . . . 17
28	26, 13, 27	rnghomadd 16123	. . . . . . . . . . . . . . . 16 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$
29		f1ocnvdm 4860	. . . . . . . . . . . . . . . . 17 $/\$
30		f1ocnvdm 4860	. . . . . . . . . . . . . . . . 17 $/\$
31	29, 30	anim12da 15647	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
32	28, 31	sylan2 500	. . . . . . . . . . . . . . 15 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
33	32	exp32 408	. . . . . . . . . . . . . 14 Ring $/\$ Ring $/\$ RngHom $/\$
34	33	3expa 1067	. . . . . . . . . . . . 13 Ring $/\$ Ring $/\$ RngHom $/\$
35	34	impr 422	. . . . . . . . . . . 12 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$
36	35	imp 377	. . . . . . . . . . 11 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
37		f1ocnvfv2 4855	. . . . . . . . . . . . . . . 16 $/\$
38	37	ancoms 484	. . . . . . . . . . . . . . 15 $/\$
39		eqid 1884	. . . . . . . . . . . . . . . . 17
40	27, 39	ringgcl 9477	. . . . . . . . . . . . . . . 16 Ring $/\$ $/\$
41	40	3expb 1068	. . . . . . . . . . . . . . 15 Ring $/\$ $/\$
42	38, 41	sylan 497	. . . . . . . . . . . . . 14 Ring $/\$ $/\$ $/\$
43	42	an1rs 547	. . . . . . . . . . . . 13 Ring $/\$ $/\$ $/\$
44	43	adantlll 432	. . . . . . . . . . . 12 Ring $/\$ Ring $/\$ $/\$ $/\$
45	44	adantlrl 434	. . . . . . . . . . 11 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
46	25, 36, 45	3eqtr4rd 1939	. . . . . . . . . 10 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
47		f1of1 4634	. . . . . . . . . . . . 13
48	47	ad2antlr 441	. . . . . . . . . . . 12 Ring $/\$ Ring $/\$ $/\$ $/\$
49		f1ocnvdm 4860	. . . . . . . . . . . . . . . 16 $/\$
50	49	ancoms 484	. . . . . . . . . . . . . . 15 $/\$
51	50, 41	sylan 497	. . . . . . . . . . . . . 14 Ring $/\$ $/\$ $/\$
52	51	an1rs 547	. . . . . . . . . . . . 13 Ring $/\$ $/\$ $/\$
53	52	adantlll 432	. . . . . . . . . . . 12 Ring $/\$ Ring $/\$ $/\$ $/\$
54	26, 13	ringgcl 9477	. . . . . . . . . . . . . . . 16 Ring $/\$ $/\$
55	54	3expb 1068	. . . . . . . . . . . . . . 15 Ring $/\$ $/\$
56	55, 31	sylan2 500	. . . . . . . . . . . . . 14 Ring $/\$ $/\$ $/\$
57	56	anassrs 489	. . . . . . . . . . . . 13 Ring $/\$ $/\$ $/\$
58	57	adantllr 433	. . . . . . . . . . . 12 Ring $/\$ Ring $/\$ $/\$ $/\$
59		f1fveq 4852	. . . . . . . . . . . 12 $/\$ $/\$
60	48, 53, 58, 59	syl12anc 1098	. . . . . . . . . . 11 Ring $/\$ Ring $/\$ $/\$ $/\$
61	60	adantlrl 434	. . . . . . . . . 10 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
62	46, 61	mpbid 212	. . . . . . . . 9 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
63		opreq12 4891	. . . . . . . . . . . . . 14 $/\$
64	21, 63	syl 12	. . . . . . . . . . . . 13 $/\$ $/\$
65	64	adantll 428	. . . . . . . . . . . 12 RngHom $/\$ $/\$ $/\$
66	65	adantll 428	. . . . . . . . . . 11 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
67	26, 13, 5, 7	rnghommul 16124	. . . . . . . . . . . . . . . 16 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$
68	67, 31	sylan2 500	. . . . . . . . . . . . . . 15 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
69	68	exp32 408	. . . . . . . . . . . . . 14 Ring $/\$ Ring $/\$ RngHom $/\$
70	69	3expa 1067	. . . . . . . . . . . . 13 Ring $/\$ Ring $/\$ RngHom $/\$
71	70	impr 422	. . . . . . . . . . . 12 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$
72	71	imp 377	. . . . . . . . . . 11 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
73		f1ocnvfv2 4855	. . . . . . . . . . . . . . . 16 $/\$
74	73	ancoms 484	. . . . . . . . . . . . . . 15 $/\$
75	27, 7, 39	ringcl 9468	. . . . . . . . . . . . . . . 16 Ring $/\$ $/\$
76	75	3expb 1068	. . . . . . . . . . . . . . 15 Ring $/\$ $/\$
77	74, 76	sylan 497	. . . . . . . . . . . . . 14 Ring $/\$ $/\$ $/\$
78	77	an1rs 547	. . . . . . . . . . . . 13 Ring $/\$ $/\$ $/\$
79	78	adantlll 432	. . . . . . . . . . . 12 Ring $/\$ Ring $/\$ $/\$ $/\$
80	79	adantlrl 434	. . . . . . . . . . 11 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
81	66, 72, 80	3eqtr4rd 1939	. . . . . . . . . 10 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
82		f1ocnvdm 4860	. . . . . . . . . . . . . . . 16 $/\$
83	82	ancoms 484	. . . . . . . . . . . . . . 15 $/\$
84	83, 76	sylan 497	. . . . . . . . . . . . . 14 Ring $/\$ $/\$ $/\$
85	84	an1rs 547	. . . . . . . . . . . . 13 Ring $/\$ $/\$ $/\$
86	85	adantlll 432	. . . . . . . . . . . 12 Ring $/\$ Ring $/\$ $/\$ $/\$
87	26, 5, 13	ringcl 9468	. . . . . . . . . . . . . . . 16 Ring $/\$ $/\$
88	87	3expb 1068	. . . . . . . . . . . . . . 15 Ring $/\$ $/\$
89	88, 31	sylan2 500	. . . . . . . . . . . . . 14 Ring $/\$ $/\$ $/\$
90	89	anassrs 489	. . . . . . . . . . . . 13 Ring $/\$ $/\$ $/\$
91	90	adantllr 433	. . . . . . . . . . . 12 Ring $/\$ Ring $/\$ $/\$ $/\$
92		f1fveq 4852	. . . . . . . . . . . 12 $/\$ $/\$
93	48, 86, 91, 92	syl12anc 1098	. . . . . . . . . . 11 Ring $/\$ Ring $/\$ $/\$ $/\$
94	93	adantlrl 434	. . . . . . . . . 10 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
95	81, 94	mpbid 212	. . . . . . . . 9 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$
96	62, 95	jca 310	. . . . . . . 8 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ $/\$ $/\$
97	96	r19.21aivva 15653	. . . . . . 7 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$
98	4, 18, 97	3jca 1050	. . . . . 6 Ring $/\$ Ring $/\$ RngHom $/\$ $/\$ Id Id $/\$ $/\$
99	27, 7, 39, 8, 26, 5, 13, 6	isrnghom 16119	. . . . . . . 8 Ring $/\$ Ring RngHom $/\$ Id Id $/\$ $/\$
100	99	ancoms 484	. . . . . . 7 Ring $/\$ Ring RngHom $/\$ Id Id $/\$ $/\$
101	100	adantr 425	. . . . . 6 Ring $/\$ Ring $/\$ RngHom $/\$ RngHom $/\$ Id Id $/\$ $/\$
102	98, 101	mpbird 213	. . . . 5 Ring $/\$ Ring $/\$ RngHom $/\$ RngHom
103	1	ad2antll 443	. . . . 5 Ring $/\$ Ring $/\$ RngHom $/\$
104	102, 103	jca 310	. . . 4 Ring $/\$ Ring $/\$ RngHom $/\$ RngHom $/\$
105	104	ex 402	. . 3 Ring $/\$ Ring RngHom $/\$ RngHom $/\$
106	26, 13, 27, 39	isrngiso 16132	. . 3 Ring $/\$ Ring RngIso RngHom $/\$
107	27, 39, 26, 13	isrngiso 16132	. . . 4 Ring $/\$ Ring RngIso RngHom $/\$
108	107	ancoms 484	. . 3 Ring $/\$ Ring RngIso RngHom $/\$
109	105, 106, 108	3imtr4d 602	. 2 Ring $/\$ Ring RngIso RngIso
110	109	3impia 1064	1 Ring $/\$ Ring $/\$ RngIso RngIso

Colors of variables: wff set class

Syntax hints:

wi 3

wb 163 $/\$ wa 240 $/\$ w3a 858

wceq 1298

wcel 1300

wral 2105

ccnv 3985

crn 3987

wf 3994

wf1 3995

wf1o 3997

cfv 3998 (class class class)co 4884

c1st 5018

c2nd 5019 Idcgi 9312 Ringcring 9463 RngHom crnghom 16114 RngIso crngiso 16115

This theorem is referenced by: riscer 16142

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-f1 4011 df-fo 4012 df-f1o 4013 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 df-rngiso 16130