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 32209

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 32207	. 2 $/\$ $\$ $\$
6		isdivrng2.5	. . . . . . 7 GId
7	1, 2, 4, 3, 6	dvrunz 26173	. . . . . 6
8	5, 7	sylbir 217	. . . . 5 $/\$ $\$ $\$
9		grporndm 25950	. . . . . . . . . . . 12 $\$ $\$ $\$ $\$ $\$ $\$
10	9	adantl 468	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
11		difss 3562	. . . . . . . . . . . . . . . . 17 $\$
12		xpss12 4943	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$
13	11, 11, 12	mp2an 679	. . . . . . . . . . . . . . . 16 $\$ $\$
14	1, 2, 4	rngosm 26121	. . . . . . . . . . . . . . . . 17
15		fdm 5738	. . . . . . . . . . . . . . . . 17
16	14, 15	syl 17	. . . . . . . . . . . . . . . 16
17	13, 16	syl5sseqr 3483	. . . . . . . . . . . . . . 15 $\$ $\$
18	17	adantr 467	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$ $\$
19		ssdmres 5129	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ $\$ $\$
20	18, 19	sylib 200	. . . . . . . . . . . . 13 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
21	20	dmeqd 5040	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
22		dmxpid 5057	. . . . . . . . . . . 12 $\$ $\$ $\$
23	21, 22	syl6eq 2503	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$
24	10, 23	eqtrd 2487	. . . . . . . . . 10 $/\$ $\$ $\$ $\$ $\$ $\$
25	24	eleq2d 2516	. . . . . . . . 9 $/\$ $\$ $\$ $\$ $\$ $\$
26	25	biimpar 488	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
27		eqid 2453	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
28		eqid 2453	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
29	27, 28	grpoinvcl 25966	. . . . . . . . . 10 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
30	29	adantll 721	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
31		eqid 2453	. . . . . . . . . . . 12 GId $\$ $\$ GId $\$ $\$
32	27, 31, 28	grpolinv 25968	. . . . . . . . . . 11 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
33	32	adantll 721	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
34	2	rngomndo 26161	. . . . . . . . . . . . . 14 MndOp
35		mndomgmid 26082	. . . . . . . . . . . . . 14 MndOp
36	34, 35	syl 17	. . . . . . . . . . . . 13
37	36	adantr 467	. . . . . . . . . . . 12 $/\$ $\$ $\$
38	11, 4	sseqtri 3466	. . . . . . . . . . . . . 14 $\$
39	2, 1	rngorn1eq 26160	. . . . . . . . . . . . . 14
40	38, 39	syl5sseq 3482	. . . . . . . . . . . . 13 $\$
41	40	adantr 467	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
42	1	rneqi 5064	. . . . . . . . . . . . . . . 16
43	4, 42	eqtri 2475	. . . . . . . . . . . . . . 15
44	43, 2, 6	rngo1cl 26169	. . . . . . . . . . . . . 14
45	44	adantr 467	. . . . . . . . . . . . 13 $/\$ $\$ $\$
46		eldifsn 4100	. . . . . . . . . . . . 13 $\$ $/\$
47	45, 8, 46	sylanbrc 671	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
48		grpomndo 26086	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ MndOp
49		mndoismgmOLD 26081	. . . . . . . . . . . . . 14 $\$ $\$ MndOp $\$ $\$
50	48, 49	syl 17	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
51	50	adantl 468	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$
52		eqid 2453	. . . . . . . . . . . . 13
53		eqid 2453	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
54	52, 6, 53	exidresid 32189	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
55	37, 41, 47, 51, 54	syl31anc 1272	. . . . . . . . . . 11 $/\$ $\$ $\$ GId $\$ $\$
56	55	adantr 467	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
57	33, 56	eqtrd 2487	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
58		oveq1 6302	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
59	58	eqeq1d 2455	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
60	59	rspcev 3152	. . . . . . . . 9 $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
61	30, 57, 60	syl2anc 667	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
62	26, 61	syldan 473	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
63	24	adantr 467	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
64	63	rexeqdv 2996	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
65		ovres 6441	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
66	65	ancoms 455	. . . . . . . . . . 11 $\$ $/\$ $\$ $\$ $\$
67	66	eqeq1d 2455	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
68	67	rexbidva 2900	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$
69	68	adantl 468	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
70	64, 69	bitrd 257	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
71	62, 70	mpbid 214	. . . . . 6 $/\$ $\$ $\$ $/\$ $\$ $\$
72	71	ralrimiva 2804	. . . . 5 $/\$ $\$ $\$ $\$ $\$
73	8, 72	jca 535	. . . 4 $/\$ $\$ $\$ $/\$ $\$ $\$
74		fvex 5880	. . . . . . . . 9
75	1, 74	eqeltri 2527	. . . . . . . 8
76	75	rnex 6732	. . . . . . 7
77	4, 76	eqeltri 2527	. . . . . 6
78		difexg 4554	. . . . . 6 $\$
79	77, 78	mp1i 13	. . . . 5 $/\$ $/\$ $\$ $\$ $\$
80		ffn 5733	. . . . . . . . 9
81	14, 80	syl 17	. . . . . . . 8
82	81	adantr 467	. . . . . . 7 $/\$ $/\$ $\$ $\$
83		fnssres 5694	. . . . . . 7 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
84	82, 13, 83	sylancl 669	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
85		ovres 6441	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
86	85	adantl 468	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
87		eldifi 3557	. . . . . . . . . . . 12 $\$
88		eldifi 3557	. . . . . . . . . . . 12 $\$
89	87, 88	anim12i 570	. . . . . . . . . . 11 $\$ $/\$ $\$ $/\$
90	1, 2, 4	rngocl 26122	. . . . . . . . . . . 12 $/\$ $/\$
91	90	3expb 1210	. . . . . . . . . . 11 $/\$ $/\$
92	89, 91	sylan2 477	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
93	92	adantlr 722	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
94		oveq2 6303	. . . . . . . . . . . . . . . 16
95	94	eqeq1d 2455	. . . . . . . . . . . . . . 15
96	95	rexbidv 2903	. . . . . . . . . . . . . 14 $\$ $\$
97	96	rspcv 3148	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
98	97	imdistanri 698	. . . . . . . . . . . 12 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$
99		eldifsn 4100	. . . . . . . . . . . . . . 15 $\$ $/\$
100		ssrexv 3496	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
101	11, 100	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$
102	1, 2, 3, 4, 6	zerdivemp1x 32206	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
103	101, 102	syl3an3 1304	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
104	87, 103	syl3an2 1303	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $\$
105	104	3expb 1210	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$ $\$
106	105	imp 431	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $/\$
107	106	necon3d 2647	. . . . . . . . . . . . . . . 16 $/\$ $\$ $/\$ $\$ $/\$
108	107	impr 625	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $\$ $/\$ $/\$
109	99, 108	sylan2b 478	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\$ $/\$ $\$
110	109	an32s 814	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $/\$ $\$
111	110	ancom2s 812	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $/\$ $\$
112	98, 111	sylan2 477	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
113	112	an42s 837	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
114	113	adantlrl 727	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
115		eldifsn 4100	. . . . . . . . 9 $\$ $/\$
116	93, 114, 115	sylanbrc 671	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
117	86, 116	eqeltrd 2531	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
118	117	ralrimivva 2811	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
119		ffnov 6405	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
120	84, 118, 119	sylanbrc 671	. . . . 5 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
121	116	3adantr3 1170	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
122		simpr3 1017	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
123	121, 122	ovresd 6442	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
124	85	3adant3 1029	. . . . . . . 8 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
125	124	adantl 468	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
126	125	oveq1d 6310	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
127		ovres 6441	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
128	127	3adant1 1027	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
129	128	adantl 468	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
130	129	oveq2d 6311	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
131		simpr1 1015	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
132		fovrn 6444	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
133	132	3adant3r1 1218	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
134	120, 133	sylan 474	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
135	131, 134	ovresd 6442	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
136		eldifi 3557	. . . . . . . . . 10 $\$
137	87, 88, 136	3anim123i 1194	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
138	1, 2, 4	rngoass 26127	. . . . . . . . 9 $/\$ $/\$ $/\$
139	137, 138	sylan2 477	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $/\$ $\$
140	139	adantlr 722	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
141	130, 135, 140	3eqtr4d 2497	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
142	123, 126, 141	3eqtr4d 2497	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
143	44	anim1i 572	. . . . . . 7 $/\$ $/\$
144	143, 46	sylibr 216	. . . . . 6 $/\$ $\$
145	144	adantrr 724	. . . . 5 $/\$ $/\$ $\$ $\$ $\$
146		ovres 6441	. . . . . . . 8 $\$ $/\$ $\$ $\$ $\$
147	144, 146	sylan 474	. . . . . . 7 $/\$ $/\$ $\$ $\$ $\$
148	2, 43, 6	rngolidm 26164	. . . . . . . . 9 $/\$
149	87, 148	sylan2 477	. . . . . . . 8 $/\$ $\$
150	149	adantlr 722	. . . . . . 7 $/\$ $/\$ $\$
151	147, 150	eqtrd 2487	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$
152	151	adantlrr 728	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
153	96	rspcva 3150	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
154		oveq1 6302	. . . . . . . . . . . 12
155	154	eqeq1d 2455	. . . . . . . . . . 11
156	155	cbvrexv 3022	. . . . . . . . . 10 $\$ $\$
157		ovres 6441	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
158	157	eqeq1d 2455	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $\$ $\$
159	158	ancoms 455	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
160	159	rexbidva 2900	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $\$
161	160	biimpar 488	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$ $\$
162	156, 161	sylan2b 478	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$ $\$
163	153, 162	syldan 473	. . . . . . . 8 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
164	163	ancoms 455	. . . . . . 7 $\$ $\$ $/\$ $\$ $\$ $\$ $\$
165	164	adantll 721	. . . . . 6 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
166	165	adantlrl 727	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
167	79, 120, 142, 145, 152, 166	isgrpda 26037	. . . 4 $/\$ $/\$ $\$ $\$ $\$ $\$
168	73, 167	impbida 844	. . 3 $\$ $\$ $/\$ $\$ $\$
169	168	pm5.32i 643	. 2 $/\$ $\$ $\$ $/\$ $/\$ $\$ $\$
170	5, 169	bitri 253	1 $/\$ $/\$ $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1446

wcel 1889

wne 2624

wral 2739

wrex 2740

cvv 3047 $\$ cdif 3403

cin 3405

wss 3406

csn 3970

cxp 4835

cdm 4837

crn 4838

cres 4839

wfn 5580

wf 5581

cfv 5585 (class class class)co 6295

c1st 6796

c2nd 6797

cgr 25926 GIdcgi 25927

cgn 25928

cexid 26054

cmagm 26058 MndOpcmndo 26077

crngo 26115

cdrng 26145

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-reu 2746 df-rmo 2747 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-iun 4283 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-riota 6257 df-ov 6298 df-om 6698 df-1st 6798 df-2nd 6799 df-1o 7187 df-er 7368 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-grpo 25931 df-gid 25932 df-ginv 25933 df-ablo 26022 df-ass 26053 df-exid 26055 df-mgmOLD 26059 df-sgrOLD 26071 df-mndo 26078 df-rngo 26116 df-drngo 26146

This theorem is referenced by: isdrngo3 32210 divrngidl 32273

W3C validator