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 28935

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 28933	. 2 $/\$ $\$ $\$
6		isdivrng2.5	. . . . . . 7 GId
7	1, 2, 4, 3, 6	dvrunz 24099	. . . . . 6
8	5, 7	sylbir 213	. . . . 5 $/\$ $\$ $\$
9		grporndm 23876	. . . . . . . . . . . 12 $\$ $\$ $\$ $\$ $\$ $\$
10	9	adantl 466	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
11		difss 3594	. . . . . . . . . . . . . . . . 17 $\$
12		xpss12 5056	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$
13	11, 11, 12	mp2an 672	. . . . . . . . . . . . . . . 16 $\$ $\$
14	1, 2, 4	rngosm 24047	. . . . . . . . . . . . . . . . 17
15		fdm 5674	. . . . . . . . . . . . . . . . 17
16	14, 15	syl 16	. . . . . . . . . . . . . . . 16
17	13, 16	syl5sseqr 3516	. . . . . . . . . . . . . . 15 $\$ $\$
18	17	adantr 465	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$ $\$
19		ssdmres 5243	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ $\$ $\$
20	18, 19	sylib 196	. . . . . . . . . . . . 13 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
21	20	dmeqd 5153	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
22		dmxpid 5170	. . . . . . . . . . . 12 $\$ $\$ $\$
23	21, 22	syl6eq 2511	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$
24	10, 23	eqtrd 2495	. . . . . . . . . 10 $/\$ $\$ $\$ $\$ $\$ $\$
25	24	eleq2d 2524	. . . . . . . . 9 $/\$ $\$ $\$ $\$ $\$ $\$
26	25	biimpar 485	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
27		eqid 2454	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
28		eqid 2454	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
29	27, 28	grpoinvcl 23892	. . . . . . . . . 10 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
30	29	adantll 713	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
31		eqid 2454	. . . . . . . . . . . 12 GId $\$ $\$ GId $\$ $\$
32	27, 31, 28	grpolinv 23894	. . . . . . . . . . 11 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
33	32	adantll 713	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
34	2	rngomndo 24087	. . . . . . . . . . . . . 14 MndOp
35		mndomgmid 24008	. . . . . . . . . . . . . 14 MndOp
36	34, 35	syl 16	. . . . . . . . . . . . 13
37	36	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $\$
38	11, 4	sseqtri 3499	. . . . . . . . . . . . . 14 $\$
39	2, 1	rngorn1eq 24086	. . . . . . . . . . . . . 14
40	38, 39	syl5sseq 3515	. . . . . . . . . . . . 13 $\$
41	40	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
42	1	rneqi 5177	. . . . . . . . . . . . . . . 16
43	4, 42	eqtri 2483	. . . . . . . . . . . . . . 15
44	43, 2, 6	rngo1cl 24095	. . . . . . . . . . . . . 14
45	44	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$ $\$
46		eldifsn 4111	. . . . . . . . . . . . 13 $\$ $/\$
47	45, 8, 46	sylanbrc 664	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
48		grpomndo 24012	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ MndOp
49		mndoismgm 24007	. . . . . . . . . . . . . 14 $\$ $\$ MndOp $\$ $\$
50	48, 49	syl 16	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
51	50	adantl 466	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$
52		eqid 2454	. . . . . . . . . . . . 13
53		eqid 2454	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
54	52, 6, 53	exidresid 28915	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
55	37, 41, 47, 51, 54	syl31anc 1222	. . . . . . . . . . 11 $/\$ $\$ $\$ GId $\$ $\$
56	55	adantr 465	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
57	33, 56	eqtrd 2495	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
58		oveq1 6210	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
59	58	eqeq1d 2456	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
60	59	rspcev 3179	. . . . . . . . 9 $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
61	30, 57, 60	syl2anc 661	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
62	26, 61	syldan 470	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
63	24	adantr 465	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
64	63	rexeqdv 3030	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
65		ovres 6343	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
66	65	ancoms 453	. . . . . . . . . . 11 $\$ $/\$ $\$ $\$ $\$
67	66	eqeq1d 2456	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
68	67	rexbidva 2865	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$
69	68	adantl 466	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
70	64, 69	bitrd 253	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
71	62, 70	mpbid 210	. . . . . 6 $/\$ $\$ $\$ $/\$ $\$ $\$
72	71	ralrimiva 2830	. . . . 5 $/\$ $\$ $\$ $\$ $\$
73	8, 72	jca 532	. . . 4 $/\$ $\$ $\$ $/\$ $\$ $\$
74		fvex 5812	. . . . . . . . 9
75	1, 74	eqeltri 2538	. . . . . . . 8
76	75	rnex 6625	. . . . . . 7
77	4, 76	eqeltri 2538	. . . . . 6
78		difexg 4551	. . . . . 6 $\$
79	77, 78	mp1i 12	. . . . 5 $/\$ $/\$ $\$ $\$ $\$
80		ffn 5670	. . . . . . . . 9
81	14, 80	syl 16	. . . . . . . 8
82	81	adantr 465	. . . . . . 7 $/\$ $/\$ $\$ $\$
83		fnssres 5635	. . . . . . 7 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
84	82, 13, 83	sylancl 662	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
85		ovres 6343	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
86	85	adantl 466	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
87		eldifi 3589	. . . . . . . . . . . 12 $\$
88		eldifi 3589	. . . . . . . . . . . 12 $\$
89	87, 88	anim12i 566	. . . . . . . . . . 11 $\$ $/\$ $\$ $/\$
90	1, 2, 4	rngocl 24048	. . . . . . . . . . . 12 $/\$ $/\$
91	90	3expb 1189	. . . . . . . . . . 11 $/\$ $/\$
92	89, 91	sylan2 474	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
93	92	adantlr 714	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
94		oveq2 6211	. . . . . . . . . . . . . . . 16
95	94	eqeq1d 2456	. . . . . . . . . . . . . . 15
96	95	rexbidv 2868	. . . . . . . . . . . . . 14 $\$ $\$
97	96	rspcv 3175	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
98	97	imdistanri 691	. . . . . . . . . . . 12 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$
99		eldifsn 4111	. . . . . . . . . . . . . . 15 $\$ $/\$
100		ssrexv 3528	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
101	11, 100	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$
102	1, 2, 3, 4, 6	zerdivemp1x 28932	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
103	101, 102	syl3an3 1254	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
104	87, 103	syl3an2 1253	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $\$
105	104	3expb 1189	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$ $\$
106	105	imp 429	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $/\$
107	106	necon3d 2676	. . . . . . . . . . . . . . . 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 823	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
114	113	adantlrl 719	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
115		eldifsn 4111	. . . . . . . . 9 $\$ $/\$
116	93, 114, 115	sylanbrc 664	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
117	86, 116	eqeltrd 2542	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
118	117	ralrimivva 2914	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
119		ffnov 6307	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
120	84, 118, 119	sylanbrc 664	. . . . 5 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
121	116	3adantr3 1149	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
122		simpr3 996	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
123	121, 122	ovresd 6344	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
124	85	3adant3 1008	. . . . . . . 8 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
125	124	adantl 466	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
126	125	oveq1d 6218	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
127		ovres 6343	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
128	127	3adant1 1006	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
129	128	adantl 466	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
130	129	oveq2d 6219	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
131		simpr1 994	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
132		fovrn 6346	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
133	132	3adant3r1 1197	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
134	120, 133	sylan 471	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
135	131, 134	ovresd 6344	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
136		eldifi 3589	. . . . . . . . . 10 $\$
137	87, 88, 136	3anim123i 1173	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
138	1, 2, 4	rngoass 24053	. . . . . . . . 9 $/\$ $/\$ $/\$
139	137, 138	sylan2 474	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $/\$ $\$
140	139	adantlr 714	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
141	130, 135, 140	3eqtr4d 2505	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
142	123, 126, 141	3eqtr4d 2505	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
143	44	anim1i 568	. . . . . . 7 $/\$ $/\$
144	143, 46	sylibr 212	. . . . . 6 $/\$ $\$
145	144	adantrr 716	. . . . 5 $/\$ $/\$ $\$ $\$ $\$
146		ovres 6343	. . . . . . . 8 $\$ $/\$ $\$ $\$ $\$
147	144, 146	sylan 471	. . . . . . 7 $/\$ $/\$ $\$ $\$ $\$
148	2, 43, 6	rngolidm 24090	. . . . . . . . 9 $/\$
149	87, 148	sylan2 474	. . . . . . . 8 $/\$ $\$
150	149	adantlr 714	. . . . . . 7 $/\$ $/\$ $\$
151	147, 150	eqtrd 2495	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$
152	151	adantlrr 720	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
153	96	rspcva 3177	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
154		oveq1 6210	. . . . . . . . . . . 12
155	154	eqeq1d 2456	. . . . . . . . . . 11
156	155	cbvrexv 3054	. . . . . . . . . 10 $\$ $\$
157		ovres 6343	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
158	157	eqeq1d 2456	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $\$ $\$
159	158	ancoms 453	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
160	159	rexbidva 2865	. . . . . . . . . . 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 23963	. . . 4 $/\$ $/\$ $\$ $\$ $\$ $\$
168	73, 167	impbida 828	. . 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 965

wceq 1370

wcel 1758

wne 2648

wral 2799

wrex 2800

cvv 3078 $\$ cdif 3436

cin 3438

wss 3439

csn 3988

cxp 4949

cdm 4951

crn 4952

cres 4953

wfn 5524

wf 5525

cfv 5529 (class class class)co 6203

c1st 6688

c2nd 6689

cgr 23852 GIdcgi 23853

cgn 23854

cexid 23980

cmagm 23984 MndOpcmndo 24003

crngo 24041

cdrng 24071

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4514 ax-sep 4524 ax-nul 4532 ax-pow 4581 ax-pr 4642 ax-un 6485

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-ral 2804 df-rex 2805 df-reu 2806 df-rmo 2807 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3399 df-dif 3442 df-un 3444 df-in 3446 df-ss 3453 df-pss 3455 df-nul 3749 df-if 3903 df-pw 3973 df-sn 3989 df-pr 3991 df-tp 3993 df-op 3995 df-uni 4203 df-iun 4284 df-br 4404 df-opab 4462 df-mpt 4463 df-tr 4497 df-eprel 4743 df-id 4747 df-po 4752 df-so 4753 df-fr 4790 df-we 4792 df-ord 4833 df-on 4834 df-lim 4835 df-suc 4836 df-xp 4957 df-rel 4958 df-cnv 4959 df-co 4960 df-dm 4961 df-rn 4962 df-res 4963 df-ima 4964 df-iota 5492 df-fun 5531 df-fn 5532 df-f 5533 df-f1 5534 df-fo 5535 df-f1o 5536 df-fv 5537 df-riota 6164 df-ov 6206 df-om 6590 df-1st 6690 df-2nd 6691 df-1o 7033 df-er 7214 df-en 7424 df-dom 7425 df-sdom 7426 df-fin 7427 df-grpo 23857 df-gid 23858 df-ginv 23859 df-ablo 23948 df-ass 23979 df-exid 23981 df-mgm 23985 df-sgr 23997 df-mndo 24004 df-rngo 24042 df-drngo 24072

This theorem is referenced by: isdrngo3 28936 divrngidl 28999

W3C validator