isdrngo2 - Mathbox for Jeff Madsen

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

Theorem isdrngo2 32261

Description: A division ring is a ring in which

and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010.)

**Hypotheses**
Ref	Expression
isdivrng1.1
isdivrng1.2
isdivrng1.3	GId
isdivrng1.4
isdivrng2.5	GId

**Assertion**
Ref	Expression
isdrngo2	$/\$ $/\$ $\$ $\$

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem isdrngo2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isdivrng1.1	. . 3
2		isdivrng1.2	. . 3
3		isdivrng1.3	. . 3 GId
4		isdivrng1.4	. . 3
5	1, 2, 3, 4	isdrngo1 32259	. 2 $/\$ $\$ $\$
6		isdivrng2.5	. . . . . . 7 GId
7	1, 2, 4, 3, 6	dvrunz 26242	. . . . . 6
8	5, 7	sylbir 218	. . . . 5 $/\$ $\$ $\$
9		grporndm 26019	. . . . . . . . . . . 12 $\$ $\$ $\$ $\$ $\$ $\$
10	9	adantl 473	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
11		difss 3549	. . . . . . . . . . . . . . . . 17 $\$
12		xpss12 4945	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$
13	11, 11, 12	mp2an 686	. . . . . . . . . . . . . . . 16 $\$ $\$
14	1, 2, 4	rngosm 26190	. . . . . . . . . . . . . . . . 17
15		fdm 5745	. . . . . . . . . . . . . . . . 17
16	14, 15	syl 17	. . . . . . . . . . . . . . . 16
17	13, 16	syl5sseqr 3467	. . . . . . . . . . . . . . 15 $\$ $\$
18	17	adantr 472	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$ $\$
19		ssdmres 5132	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ $\$ $\$
20	18, 19	sylib 201	. . . . . . . . . . . . 13 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
21	20	dmeqd 5042	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
22		dmxpid 5060	. . . . . . . . . . . 12 $\$ $\$ $\$
23	21, 22	syl6eq 2521	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$
24	10, 23	eqtrd 2505	. . . . . . . . . 10 $/\$ $\$ $\$ $\$ $\$ $\$
25	24	eleq2d 2534	. . . . . . . . 9 $/\$ $\$ $\$ $\$ $\$ $\$
26	25	biimpar 493	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
27		eqid 2471	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
28		eqid 2471	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
29	27, 28	grpoinvcl 26035	. . . . . . . . . 10 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
30	29	adantll 728	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
31		eqid 2471	. . . . . . . . . . . 12 GId $\$ $\$ GId $\$ $\$
32	27, 31, 28	grpolinv 26037	. . . . . . . . . . 11 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
33	32	adantll 728	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
34	2	rngomndo 26230	. . . . . . . . . . . . . 14 MndOp
35		mndomgmid 26151	. . . . . . . . . . . . . 14 MndOp
36	34, 35	syl 17	. . . . . . . . . . . . 13
37	36	adantr 472	. . . . . . . . . . . 12 $/\$ $\$ $\$
38	11, 4	sseqtri 3450	. . . . . . . . . . . . . 14 $\$
39	2, 1	rngorn1eq 26229	. . . . . . . . . . . . . 14
40	38, 39	syl5sseq 3466	. . . . . . . . . . . . 13 $\$
41	40	adantr 472	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
42	1	rneqi 5067	. . . . . . . . . . . . . . . 16
43	4, 42	eqtri 2493	. . . . . . . . . . . . . . 15
44	43, 2, 6	rngo1cl 26238	. . . . . . . . . . . . . 14
45	44	adantr 472	. . . . . . . . . . . . 13 $/\$ $\$ $\$
46		eldifsn 4088	. . . . . . . . . . . . 13 $\$ $/\$
47	45, 8, 46	sylanbrc 677	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
48		grpomndo 26155	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ MndOp
49		mndoismgmOLD 26150	. . . . . . . . . . . . . 14 $\$ $\$ MndOp $\$ $\$
50	48, 49	syl 17	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
51	50	adantl 473	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$
52		eqid 2471	. . . . . . . . . . . . 13
53		eqid 2471	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
54	52, 6, 53	exidresid 32241	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
55	37, 41, 47, 51, 54	syl31anc 1295	. . . . . . . . . . 11 $/\$ $\$ $\$ GId $\$ $\$
56	55	adantr 472	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
57	33, 56	eqtrd 2505	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
58		oveq1 6315	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
59	58	eqeq1d 2473	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
60	59	rspcev 3136	. . . . . . . . 9 $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
61	30, 57, 60	syl2anc 673	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
62	26, 61	syldan 478	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
63	24	adantr 472	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
64	63	rexeqdv 2980	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
65		ovres 6455	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
66	65	ancoms 460	. . . . . . . . . . 11 $\$ $/\$ $\$ $\$ $\$
67	66	eqeq1d 2473	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
68	67	rexbidva 2889	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$
69	68	adantl 473	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
70	64, 69	bitrd 261	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
71	62, 70	mpbid 215	. . . . . 6 $/\$ $\$ $\$ $/\$ $\$ $\$
72	71	ralrimiva 2809	. . . . 5 $/\$ $\$ $\$ $\$ $\$
73	8, 72	jca 541	. . . 4 $/\$ $\$ $\$ $/\$ $\$ $\$
74		fvex 5889	. . . . . . . . 9
75	1, 74	eqeltri 2545	. . . . . . . 8
76	75	rnex 6746	. . . . . . 7
77	4, 76	eqeltri 2545	. . . . . 6
78		difexg 4545	. . . . . 6 $\$
79	77, 78	mp1i 13	. . . . 5 $/\$ $/\$ $\$ $\$ $\$
80		ffn 5739	. . . . . . . . 9
81	14, 80	syl 17	. . . . . . . 8
82	81	adantr 472	. . . . . . 7 $/\$ $/\$ $\$ $\$
83		fnssres 5699	. . . . . . 7 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
84	82, 13, 83	sylancl 675	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
85		ovres 6455	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
86	85	adantl 473	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
87		eldifi 3544	. . . . . . . . . . . 12 $\$
88		eldifi 3544	. . . . . . . . . . . 12 $\$
89	87, 88	anim12i 576	. . . . . . . . . . 11 $\$ $/\$ $\$ $/\$
90	1, 2, 4	rngocl 26191	. . . . . . . . . . . 12 $/\$ $/\$
91	90	3expb 1232	. . . . . . . . . . 11 $/\$ $/\$
92	89, 91	sylan2 482	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
93	92	adantlr 729	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
94		oveq2 6316	. . . . . . . . . . . . . . . 16
95	94	eqeq1d 2473	. . . . . . . . . . . . . . 15
96	95	rexbidv 2892	. . . . . . . . . . . . . 14 $\$ $\$
97	96	rspcv 3132	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
98	97	imdistanri 705	. . . . . . . . . . . 12 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$
99		eldifsn 4088	. . . . . . . . . . . . . . 15 $\$ $/\$
100		ssrexv 3480	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
101	11, 100	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$
102	1, 2, 3, 4, 6	zerdivemp1x 32258	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
103	101, 102	syl3an3 1327	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
104	87, 103	syl3an2 1326	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $\$
105	104	3expb 1232	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$ $\$
106	105	imp 436	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $/\$
107	106	necon3d 2664	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $/\$
108	107	impr 631	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $/\$ $/\$
109	99, 108	sylan2b 483	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $/\$ $\$
110	109	an32s 821	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $/\$ $\$
111	110	ancom2s 819	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $/\$ $\$
112	98, 111	sylan2 482	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
113	112	an42s 843	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
114	113	adantlrl 734	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
115		eldifsn 4088	. . . . . . . . 9 $\$ $/\$
116	93, 114, 115	sylanbrc 677	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
117	86, 116	eqeltrd 2549	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
118	117	ralrimivva 2814	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
119		ffnov 6419	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
120	84, 118, 119	sylanbrc 677	. . . . 5 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
121	116	3adantr3 1191	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
122		simpr3 1038	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
123	121, 122	ovresd 6456	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
124	85	3adant3 1050	. . . . . . . 8 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
125	124	adantl 473	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
126	125	oveq1d 6323	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
127		ovres 6455	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
128	127	3adant1 1048	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
129	128	adantl 473	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
130	129	oveq2d 6324	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
131		simpr1 1036	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
132		fovrn 6458	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
133	132	3adant3r1 1240	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
134	120, 133	sylan 479	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
135	131, 134	ovresd 6456	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
136		eldifi 3544	. . . . . . . . . 10 $\$
137	87, 88, 136	3anim123i 1215	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
138	1, 2, 4	rngoass 26196	. . . . . . . . 9 $/\$ $/\$ $/\$
139	137, 138	sylan2 482	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $/\$ $\$
140	139	adantlr 729	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
141	130, 135, 140	3eqtr4d 2515	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
142	123, 126, 141	3eqtr4d 2515	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
143	44	anim1i 578	. . . . . . 7 $/\$ $/\$
144	143, 46	sylibr 217	. . . . . 6 $/\$ $\$
145	144	adantrr 731	. . . . 5 $/\$ $/\$ $\$ $\$ $\$
146		ovres 6455	. . . . . . . 8 $\$ $/\$ $\$ $\$ $\$
147	144, 146	sylan 479	. . . . . . 7 $/\$ $/\$ $\$ $\$ $\$
148	2, 43, 6	rngolidm 26233	. . . . . . . . 9 $/\$
149	87, 148	sylan2 482	. . . . . . . 8 $/\$ $\$
150	149	adantlr 729	. . . . . . 7 $/\$ $/\$ $\$
151	147, 150	eqtrd 2505	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$
152	151	adantlrr 735	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
153	96	rspcva 3134	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
154		oveq1 6315	. . . . . . . . . . . 12
155	154	eqeq1d 2473	. . . . . . . . . . 11
156	155	cbvrexv 3006	. . . . . . . . . 10 $\$ $\$
157		ovres 6455	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
158	157	eqeq1d 2473	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $\$ $\$
159	158	ancoms 460	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
160	159	rexbidva 2889	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $\$
161	160	biimpar 493	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$ $\$
162	156, 161	sylan2b 483	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$ $\$
163	153, 162	syldan 478	. . . . . . . 8 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
164	163	ancoms 460	. . . . . . 7 $\$ $\$ $/\$ $\$ $\$ $\$ $\$
165	164	adantll 728	. . . . . 6 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
166	165	adantlrl 734	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
167	79, 120, 142, 145, 152, 166	isgrpda 26106	. . . 4 $/\$ $/\$ $\$ $\$ $\$ $\$
168	73, 167	impbida 850	. . 3 $\$ $\$ $/\$ $\$ $\$
169	168	pm5.32i 649	. 2 $/\$ $\$ $\$ $/\$ $/\$ $\$ $\$
170	5, 169	bitri 257	1 $/\$ $/\$ $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

cvv 3031 $\$ cdif 3387

cin 3389

wss 3390

csn 3959

cxp 4837

cdm 4839

crn 4840

cres 4841

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

c1st 6810

c2nd 6811

cgr 25995 GIdcgi 25996

cgn 25997

cexid 26123

cmagm 26127 MndOpcmndo 26146

crngo 26184

cdrng 26214

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-om 6712 df-1st 6812 df-2nd 6813 df-1o 7200 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-grpo 26000 df-gid 26001 df-ginv 26002 df-ablo 26091 df-ass 26122 df-exid 26124 df-mgmOLD 26128 df-sgrOLD 26140 df-mndo 26147 df-rngo 26185 df-drngo 26215

This theorem is referenced by: isdrngo3 32262 divrngidl 32325

W3C validator