isdrngo2 - Mathbox for Jeff Madsen

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

Theorem isdrngo2 30288

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 30286	. 2 $/\$ $\$ $\$
6		isdivrng2.5	. . . . . . 7 GId
7	1, 2, 4, 3, 6	dvrunz 25258	. . . . . 6
8	5, 7	sylbir 213	. . . . 5 $/\$ $\$ $\$
9		grporndm 25035	. . . . . . . . . . . 12 $\$ $\$ $\$ $\$ $\$ $\$
10	9	adantl 466	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
11		difss 3636	. . . . . . . . . . . . . . . . 17 $\$
12		xpss12 5114	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$
13	11, 11, 12	mp2an 672	. . . . . . . . . . . . . . . 16 $\$ $\$
14	1, 2, 4	rngosm 25206	. . . . . . . . . . . . . . . . 17
15		fdm 5741	. . . . . . . . . . . . . . . . 17
16	14, 15	syl 16	. . . . . . . . . . . . . . . 16
17	13, 16	syl5sseqr 3558	. . . . . . . . . . . . . . 15 $\$ $\$
18	17	adantr 465	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$ $\$
19		ssdmres 5301	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ $\$ $\$
20	18, 19	sylib 196	. . . . . . . . . . . . 13 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
21	20	dmeqd 5211	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
22		dmxpid 5228	. . . . . . . . . . . 12 $\$ $\$ $\$
23	21, 22	syl6eq 2524	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$
24	10, 23	eqtrd 2508	. . . . . . . . . 10 $/\$ $\$ $\$ $\$ $\$ $\$
25	24	eleq2d 2537	. . . . . . . . 9 $/\$ $\$ $\$ $\$ $\$ $\$
26	25	biimpar 485	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
27		eqid 2467	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
28		eqid 2467	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
29	27, 28	grpoinvcl 25051	. . . . . . . . . 10 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
30	29	adantll 713	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
31		eqid 2467	. . . . . . . . . . . 12 GId $\$ $\$ GId $\$ $\$
32	27, 31, 28	grpolinv 25053	. . . . . . . . . . 11 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
33	32	adantll 713	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
34	2	rngomndo 25246	. . . . . . . . . . . . . 14 MndOp
35		mndomgmid 25167	. . . . . . . . . . . . . 14 MndOp
36	34, 35	syl 16	. . . . . . . . . . . . 13
37	36	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $\$
38	11, 4	sseqtri 3541	. . . . . . . . . . . . . 14 $\$
39	2, 1	rngorn1eq 25245	. . . . . . . . . . . . . 14
40	38, 39	syl5sseq 3557	. . . . . . . . . . . . 13 $\$
41	40	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
42	1	rneqi 5235	. . . . . . . . . . . . . . . 16
43	4, 42	eqtri 2496	. . . . . . . . . . . . . . 15
44	43, 2, 6	rngo1cl 25254	. . . . . . . . . . . . . 14
45	44	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$ $\$
46		eldifsn 4158	. . . . . . . . . . . . 13 $\$ $/\$
47	45, 8, 46	sylanbrc 664	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
48		grpomndo 25171	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ MndOp
49		mndoismgmOLD 25166	. . . . . . . . . . . . . 14 $\$ $\$ MndOp $\$ $\$
50	48, 49	syl 16	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
51	50	adantl 466	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$
52		eqid 2467	. . . . . . . . . . . . 13
53		eqid 2467	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
54	52, 6, 53	exidresid 30268	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
55	37, 41, 47, 51, 54	syl31anc 1231	. . . . . . . . . . 11 $/\$ $\$ $\$ GId $\$ $\$
56	55	adantr 465	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
57	33, 56	eqtrd 2508	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
58		oveq1 6302	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
59	58	eqeq1d 2469	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
60	59	rspcev 3219	. . . . . . . . 9 $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
61	30, 57, 60	syl2anc 661	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
62	26, 61	syldan 470	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
63	24	adantr 465	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
64	63	rexeqdv 3070	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
65		ovres 6437	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
66	65	ancoms 453	. . . . . . . . . . 11 $\$ $/\$ $\$ $\$ $\$
67	66	eqeq1d 2469	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
68	67	rexbidva 2975	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$
69	68	adantl 466	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
70	64, 69	bitrd 253	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
71	62, 70	mpbid 210	. . . . . 6 $/\$ $\$ $\$ $/\$ $\$ $\$
72	71	ralrimiva 2881	. . . . 5 $/\$ $\$ $\$ $\$ $\$
73	8, 72	jca 532	. . . 4 $/\$ $\$ $\$ $/\$ $\$ $\$
74		fvex 5882	. . . . . . . . 9
75	1, 74	eqeltri 2551	. . . . . . . 8
76	75	rnex 6729	. . . . . . 7
77	4, 76	eqeltri 2551	. . . . . 6
78		difexg 4601	. . . . . 6 $\$
79	77, 78	mp1i 12	. . . . 5 $/\$ $/\$ $\$ $\$ $\$
80		ffn 5737	. . . . . . . . 9
81	14, 80	syl 16	. . . . . . . 8
82	81	adantr 465	. . . . . . 7 $/\$ $/\$ $\$ $\$
83		fnssres 5700	. . . . . . 7 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
84	82, 13, 83	sylancl 662	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
85		ovres 6437	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
86	85	adantl 466	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
87		eldifi 3631	. . . . . . . . . . . 12 $\$
88		eldifi 3631	. . . . . . . . . . . 12 $\$
89	87, 88	anim12i 566	. . . . . . . . . . 11 $\$ $/\$ $\$ $/\$
90	1, 2, 4	rngocl 25207	. . . . . . . . . . . 12 $/\$ $/\$
91	90	3expb 1197	. . . . . . . . . . 11 $/\$ $/\$
92	89, 91	sylan2 474	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
93	92	adantlr 714	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
94		oveq2 6303	. . . . . . . . . . . . . . . 16
95	94	eqeq1d 2469	. . . . . . . . . . . . . . 15
96	95	rexbidv 2978	. . . . . . . . . . . . . 14 $\$ $\$
97	96	rspcv 3215	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
98	97	imdistanri 691	. . . . . . . . . . . 12 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$
99		eldifsn 4158	. . . . . . . . . . . . . . 15 $\$ $/\$
100		ssrexv 3570	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
101	11, 100	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$
102	1, 2, 3, 4, 6	zerdivemp1x 30285	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
103	101, 102	syl3an3 1263	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
104	87, 103	syl3an2 1262	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $\$
105	104	3expb 1197	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$ $\$
106	105	imp 429	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $/\$
107	106	necon3d 2691	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $/\$
108	107	impr 619	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $/\$ $/\$
109	99, 108	sylan2b 475	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $/\$ $\$
110	109	an32s 802	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $/\$ $\$
111	110	ancom2s 800	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $/\$ $\$
112	98, 111	sylan2 474	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
113	112	an42s 825	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
114	113	adantlrl 719	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
115		eldifsn 4158	. . . . . . . . 9 $\$ $/\$
116	93, 114, 115	sylanbrc 664	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
117	86, 116	eqeltrd 2555	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
118	117	ralrimivva 2888	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
119		ffnov 6401	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
120	84, 118, 119	sylanbrc 664	. . . . 5 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
121	116	3adantr3 1157	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
122		simpr3 1004	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
123	121, 122	ovresd 6438	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
124	85	3adant3 1016	. . . . . . . 8 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
125	124	adantl 466	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
126	125	oveq1d 6310	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
127		ovres 6437	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
128	127	3adant1 1014	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
129	128	adantl 466	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
130	129	oveq2d 6311	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
131		simpr1 1002	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
132		fovrn 6440	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
133	132	3adant3r1 1205	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
134	120, 133	sylan 471	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
135	131, 134	ovresd 6438	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
136		eldifi 3631	. . . . . . . . . 10 $\$
137	87, 88, 136	3anim123i 1181	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
138	1, 2, 4	rngoass 25212	. . . . . . . . 9 $/\$ $/\$ $/\$
139	137, 138	sylan2 474	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $/\$ $\$
140	139	adantlr 714	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
141	130, 135, 140	3eqtr4d 2518	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
142	123, 126, 141	3eqtr4d 2518	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
143	44	anim1i 568	. . . . . . 7 $/\$ $/\$
144	143, 46	sylibr 212	. . . . . 6 $/\$ $\$
145	144	adantrr 716	. . . . 5 $/\$ $/\$ $\$ $\$ $\$
146		ovres 6437	. . . . . . . 8 $\$ $/\$ $\$ $\$ $\$
147	144, 146	sylan 471	. . . . . . 7 $/\$ $/\$ $\$ $\$ $\$
148	2, 43, 6	rngolidm 25249	. . . . . . . . 9 $/\$
149	87, 148	sylan2 474	. . . . . . . 8 $/\$ $\$
150	149	adantlr 714	. . . . . . 7 $/\$ $/\$ $\$
151	147, 150	eqtrd 2508	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$
152	151	adantlrr 720	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
153	96	rspcva 3217	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
154		oveq1 6302	. . . . . . . . . . . 12
155	154	eqeq1d 2469	. . . . . . . . . . 11
156	155	cbvrexv 3094	. . . . . . . . . 10 $\$ $\$
157		ovres 6437	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
158	157	eqeq1d 2469	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $\$ $\$
159	158	ancoms 453	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
160	159	rexbidva 2975	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $\$
161	160	biimpar 485	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$ $\$
162	156, 161	sylan2b 475	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$ $\$
163	153, 162	syldan 470	. . . . . . . 8 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
164	163	ancoms 453	. . . . . . 7 $\$ $\$ $/\$ $\$ $\$ $\$ $\$
165	164	adantll 713	. . . . . 6 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
166	165	adantlrl 719	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
167	79, 120, 142, 145, 152, 166	isgrpda 25122	. . . 4 $/\$ $/\$ $\$ $\$ $\$ $\$
168	73, 167	impbida 830	. . 3 $\$ $\$ $/\$ $\$ $\$
169	168	pm5.32i 637	. 2 $/\$ $\$ $\$ $/\$ $/\$ $\$ $\$
170	5, 169	bitri 249	1 $/\$ $/\$ $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1379

wcel 1767

wne 2662

wral 2817

wrex 2818

cvv 3118 $\$ cdif 3478

cin 3480

wss 3481

csn 4033

cxp 5003

cdm 5005

crn 5006

cres 5007

wfn 5589

wf 5590

cfv 5594 (class class class)co 6295

c1st 6793

c2nd 6794

cgr 25011 GIdcgi 25012

cgn 25013

cexid 25139

cmagm 25143 MndOpcmndo 25162

crngo 25200

cdrng 25230

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4564 ax-sep 4574 ax-nul 4582 ax-pow 4631 ax-pr 4692 ax-un 6587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2822 df-rex 2823 df-reu 2824 df-rmo 2825 df-rab 2826 df-v 3120 df-sbc 3337 df-csb 3441 df-dif 3484 df-un 3486 df-in 3488 df-ss 3495 df-pss 3497 df-nul 3791 df-if 3946 df-pw 4018 df-sn 4034 df-pr 4036 df-tp 4038 df-op 4040 df-uni 4252 df-iun 4333 df-br 4454 df-opab 4512 df-mpt 4513 df-tr 4547 df-eprel 4797 df-id 4801 df-po 4806 df-so 4807 df-fr 4844 df-we 4846 df-ord 4887 df-on 4888 df-lim 4889 df-suc 4890 df-xp 5011 df-rel 5012 df-cnv 5013 df-co 5014 df-dm 5015 df-rn 5016 df-res 5017 df-ima 5018 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6256 df-ov 6298 df-om 6696 df-1st 6795 df-2nd 6796 df-1o 7142 df-er 7323 df-en 7529 df-dom 7530 df-sdom 7531 df-fin 7532 df-grpo 25016 df-gid 25017 df-ginv 25018 df-ablo 25107 df-ass 25138 df-exid 25140 df-mgmOLD 25144 df-sgrOLD 25156 df-mndo 25163 df-rngo 25201 df-drngo 25231

This theorem is referenced by: isdrngo3 30289 divrngidl 30352

W3C validator