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 30566

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 30564	. 2 $/\$ $\$ $\$
6		isdivrng2.5	. . . . . . 7 GId
7	1, 2, 4, 3, 6	dvrunz 25562	. . . . . 6
8	5, 7	sylbir 213	. . . . 5 $/\$ $\$ $\$
9		grporndm 25339	. . . . . . . . . . . 12 $\$ $\$ $\$ $\$ $\$ $\$
10	9	adantl 466	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
11		difss 3627	. . . . . . . . . . . . . . . . 17 $\$
12		xpss12 5117	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$
13	11, 11, 12	mp2an 672	. . . . . . . . . . . . . . . 16 $\$ $\$
14	1, 2, 4	rngosm 25510	. . . . . . . . . . . . . . . . 17
15		fdm 5741	. . . . . . . . . . . . . . . . 17
16	14, 15	syl 16	. . . . . . . . . . . . . . . 16
17	13, 16	syl5sseqr 3548	. . . . . . . . . . . . . . 15 $\$ $\$
18	17	adantr 465	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$ $\$
19		ssdmres 5305	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ $\$ $\$
20	18, 19	sylib 196	. . . . . . . . . . . . 13 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
21	20	dmeqd 5215	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
22		dmxpid 5232	. . . . . . . . . . . 12 $\$ $\$ $\$
23	21, 22	syl6eq 2514	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$
24	10, 23	eqtrd 2498	. . . . . . . . . 10 $/\$ $\$ $\$ $\$ $\$ $\$
25	24	eleq2d 2527	. . . . . . . . 9 $/\$ $\$ $\$ $\$ $\$ $\$
26	25	biimpar 485	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
27		eqid 2457	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
28		eqid 2457	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
29	27, 28	grpoinvcl 25355	. . . . . . . . . 10 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
30	29	adantll 713	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
31		eqid 2457	. . . . . . . . . . . 12 GId $\$ $\$ GId $\$ $\$
32	27, 31, 28	grpolinv 25357	. . . . . . . . . . 11 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
33	32	adantll 713	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
34	2	rngomndo 25550	. . . . . . . . . . . . . 14 MndOp
35		mndomgmid 25471	. . . . . . . . . . . . . 14 MndOp
36	34, 35	syl 16	. . . . . . . . . . . . 13
37	36	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $\$
38	11, 4	sseqtri 3531	. . . . . . . . . . . . . 14 $\$
39	2, 1	rngorn1eq 25549	. . . . . . . . . . . . . 14
40	38, 39	syl5sseq 3547	. . . . . . . . . . . . 13 $\$
41	40	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
42	1	rneqi 5239	. . . . . . . . . . . . . . . 16
43	4, 42	eqtri 2486	. . . . . . . . . . . . . . 15
44	43, 2, 6	rngo1cl 25558	. . . . . . . . . . . . . 14
45	44	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$ $\$
46		eldifsn 4157	. . . . . . . . . . . . 13 $\$ $/\$
47	45, 8, 46	sylanbrc 664	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
48		grpomndo 25475	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ MndOp
49		mndoismgmOLD 25470	. . . . . . . . . . . . . 14 $\$ $\$ MndOp $\$ $\$
50	48, 49	syl 16	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
51	50	adantl 466	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$
52		eqid 2457	. . . . . . . . . . . . 13
53		eqid 2457	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
54	52, 6, 53	exidresid 30546	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
55	37, 41, 47, 51, 54	syl31anc 1231	. . . . . . . . . . 11 $/\$ $\$ $\$ GId $\$ $\$
56	55	adantr 465	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
57	33, 56	eqtrd 2498	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
58		oveq1 6303	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
59	58	eqeq1d 2459	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
60	59	rspcev 3210	. . . . . . . . 9 $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
61	30, 57, 60	syl2anc 661	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
62	26, 61	syldan 470	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
63	24	adantr 465	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
64	63	rexeqdv 3061	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
65		ovres 6441	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
66	65	ancoms 453	. . . . . . . . . . 11 $\$ $/\$ $\$ $\$ $\$
67	66	eqeq1d 2459	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
68	67	rexbidva 2965	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$
69	68	adantl 466	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
70	64, 69	bitrd 253	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
71	62, 70	mpbid 210	. . . . . 6 $/\$ $\$ $\$ $/\$ $\$ $\$
72	71	ralrimiva 2871	. . . . 5 $/\$ $\$ $\$ $\$ $\$
73	8, 72	jca 532	. . . 4 $/\$ $\$ $\$ $/\$ $\$ $\$
74		fvex 5882	. . . . . . . . 9
75	1, 74	eqeltri 2541	. . . . . . . 8
76	75	rnex 6733	. . . . . . 7
77	4, 76	eqeltri 2541	. . . . . 6
78		difexg 4604	. . . . . 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 6441	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
86	85	adantl 466	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
87		eldifi 3622	. . . . . . . . . . . 12 $\$
88		eldifi 3622	. . . . . . . . . . . 12 $\$
89	87, 88	anim12i 566	. . . . . . . . . . 11 $\$ $/\$ $\$ $/\$
90	1, 2, 4	rngocl 25511	. . . . . . . . . . . 12 $/\$ $/\$
91	90	3expb 1197	. . . . . . . . . . 11 $/\$ $/\$
92	89, 91	sylan2 474	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
93	92	adantlr 714	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
94		oveq2 6304	. . . . . . . . . . . . . . . 16
95	94	eqeq1d 2459	. . . . . . . . . . . . . . 15
96	95	rexbidv 2968	. . . . . . . . . . . . . 14 $\$ $\$
97	96	rspcv 3206	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
98	97	imdistanri 691	. . . . . . . . . . . 12 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$
99		eldifsn 4157	. . . . . . . . . . . . . . 15 $\$ $/\$
100		ssrexv 3561	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
101	11, 100	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$
102	1, 2, 3, 4, 6	zerdivemp1x 30563	. . . . . . . . . . . . . . . . . . . . 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 2681	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $/\$
108	107	impr 619	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $/\$ $/\$
109	99, 108	sylan2b 475	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $/\$ $\$
110	109	an32s 804	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $/\$ $\$
111	110	ancom2s 802	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $/\$ $\$
112	98, 111	sylan2 474	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
113	112	an42s 827	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
114	113	adantlrl 719	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
115		eldifsn 4157	. . . . . . . . 9 $\$ $/\$
116	93, 114, 115	sylanbrc 664	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
117	86, 116	eqeltrd 2545	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
118	117	ralrimivva 2878	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
119		ffnov 6405	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
120	84, 118, 119	sylanbrc 664	. . . . 5 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
121	116	3adantr3 1157	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
122		simpr3 1004	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
123	121, 122	ovresd 6442	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
124	85	3adant3 1016	. . . . . . . 8 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
125	124	adantl 466	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
126	125	oveq1d 6311	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
127		ovres 6441	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
128	127	3adant1 1014	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
129	128	adantl 466	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
130	129	oveq2d 6312	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
131		simpr1 1002	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
132		fovrn 6444	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
133	132	3adant3r1 1205	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
134	120, 133	sylan 471	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
135	131, 134	ovresd 6442	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
136		eldifi 3622	. . . . . . . . . 10 $\$
137	87, 88, 136	3anim123i 1181	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
138	1, 2, 4	rngoass 25516	. . . . . . . . 9 $/\$ $/\$ $/\$
139	137, 138	sylan2 474	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $/\$ $\$
140	139	adantlr 714	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
141	130, 135, 140	3eqtr4d 2508	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
142	123, 126, 141	3eqtr4d 2508	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
143	44	anim1i 568	. . . . . . 7 $/\$ $/\$
144	143, 46	sylibr 212	. . . . . 6 $/\$ $\$
145	144	adantrr 716	. . . . 5 $/\$ $/\$ $\$ $\$ $\$
146		ovres 6441	. . . . . . . 8 $\$ $/\$ $\$ $\$ $\$
147	144, 146	sylan 471	. . . . . . 7 $/\$ $/\$ $\$ $\$ $\$
148	2, 43, 6	rngolidm 25553	. . . . . . . . 9 $/\$
149	87, 148	sylan2 474	. . . . . . . 8 $/\$ $\$
150	149	adantlr 714	. . . . . . 7 $/\$ $/\$ $\$
151	147, 150	eqtrd 2498	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$
152	151	adantlrr 720	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
153	96	rspcva 3208	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
154		oveq1 6303	. . . . . . . . . . . 12
155	154	eqeq1d 2459	. . . . . . . . . . 11
156	155	cbvrexv 3085	. . . . . . . . . 10 $\$ $\$
157		ovres 6441	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
158	157	eqeq1d 2459	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $\$ $\$
159	158	ancoms 453	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
160	159	rexbidva 2965	. . . . . . . . . . 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 25426	. . . 4 $/\$ $/\$ $\$ $\$ $\$ $\$
168	73, 167	impbida 832	. . 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 1395

wcel 1819

wne 2652

wral 2807

wrex 2808

cvv 3109 $\$ cdif 3468

cin 3470

wss 3471

csn 4032

cxp 5006

cdm 5008

crn 5009

cres 5010

wfn 5589

wf 5590

cfv 5594 (class class class)co 6296

c1st 6797

c2nd 6798

cgr 25315 GIdcgi 25316

cgn 25317

cexid 25443

cmagm 25447 MndOpcmndo 25466

crngo 25504

cdrng 25534

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 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 6258 df-ov 6299 df-om 6700 df-1st 6799 df-2nd 6800 df-1o 7148 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-grpo 25320 df-gid 25321 df-ginv 25322 df-ablo 25411 df-ass 25442 df-exid 25444 df-mgmOLD 25448 df-sgrOLD 25460 df-mndo 25467 df-rngo 25505 df-drngo 25535

This theorem is referenced by: isdrngo3 30567 divrngidl 30630

W3C validator