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 28717

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 28715	. 2 $/\$ $\$ $\$
6		isdivrng2.5	. . . . . . 7 GId
7	1, 2, 4, 3, 6	dvrunz 23871	. . . . . 6
8	5, 7	sylbir 213	. . . . 5 $/\$ $\$ $\$
9		grporndm 23648	. . . . . . . . . . . 12 $\$ $\$ $\$ $\$ $\$ $\$
10	9	adantl 466	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
11		difss 3478	. . . . . . . . . . . . . . . . 17 $\$
12		xpss12 4940	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$
13	11, 11, 12	mp2an 672	. . . . . . . . . . . . . . . 16 $\$ $\$
14	1, 2, 4	rngosm 23819	. . . . . . . . . . . . . . . . 17
15		fdm 5558	. . . . . . . . . . . . . . . . 17
16	14, 15	syl 16	. . . . . . . . . . . . . . . 16
17	13, 16	syl5sseqr 3400	. . . . . . . . . . . . . . 15 $\$ $\$
18	17	adantr 465	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$ $\$
19		ssdmres 5127	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ $\$ $\$
20	18, 19	sylib 196	. . . . . . . . . . . . 13 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
21	20	dmeqd 5037	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
22		dmxpid 5054	. . . . . . . . . . . 12 $\$ $\$ $\$
23	21, 22	syl6eq 2486	. . . . . . . . . . 11 $/\$ $\$ $\$ $\$ $\$ $\$
24	10, 23	eqtrd 2470	. . . . . . . . . 10 $/\$ $\$ $\$ $\$ $\$ $\$
25	24	eleq2d 2505	. . . . . . . . 9 $/\$ $\$ $\$ $\$ $\$ $\$
26	25	biimpar 485	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
27		eqid 2438	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
28		eqid 2438	. . . . . . . . . . 11 $\$ $\$ $\$ $\$
29	27, 28	grpoinvcl 23664	. . . . . . . . . 10 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
30	29	adantll 713	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
31		eqid 2438	. . . . . . . . . . . 12 GId $\$ $\$ GId $\$ $\$
32	27, 31, 28	grpolinv 23666	. . . . . . . . . . 11 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
33	32	adantll 713	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ GId $\$ $\$
34	2	rngomndo 23859	. . . . . . . . . . . . . 14 MndOp
35		mndomgmid 23780	. . . . . . . . . . . . . 14 MndOp
36	34, 35	syl 16	. . . . . . . . . . . . 13
37	36	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $\$
38	11, 4	sseqtri 3383	. . . . . . . . . . . . . 14 $\$
39	2, 1	rngorn1eq 23858	. . . . . . . . . . . . . 14
40	38, 39	syl5sseq 3399	. . . . . . . . . . . . 13 $\$
41	40	adantr 465	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
42	1	rneqi 5061	. . . . . . . . . . . . . . . 16
43	4, 42	eqtri 2458	. . . . . . . . . . . . . . 15
44	43, 2, 6	rngo1cl 23867	. . . . . . . . . . . . . 14
45	44	adantr 465	. . . . . . . . . . . . 13 $/\$ $\$ $\$
46		eldifsn 3995	. . . . . . . . . . . . 13 $\$ $/\$
47	45, 8, 46	sylanbrc 664	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$
48		grpomndo 23784	. . . . . . . . . . . . . 14 $\$ $\$ $\$ $\$ MndOp
49		mndoismgm 23779	. . . . . . . . . . . . . 14 $\$ $\$ MndOp $\$ $\$
50	48, 49	syl 16	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
51	50	adantl 466	. . . . . . . . . . . 12 $/\$ $\$ $\$ $\$ $\$
52		eqid 2438	. . . . . . . . . . . . 13
53		eqid 2438	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
54	52, 6, 53	exidresid 28697	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
55	37, 41, 47, 51, 54	syl31anc 1221	. . . . . . . . . . 11 $/\$ $\$ $\$ GId $\$ $\$
56	55	adantr 465	. . . . . . . . . 10 $/\$ $\$ $\$ $/\$ $\$ $\$ GId $\$ $\$
57	33, 56	eqtrd 2470	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
58		oveq1 6093	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
59	58	eqeq1d 2446	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
60	59	rspcev 3068	. . . . . . . . 9 $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
61	30, 57, 60	syl2anc 661	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
62	26, 61	syldan 470	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
63	24	adantr 465	. . . . . . . . 9 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
64	63	rexeqdv 2919	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
65		ovres 6225	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
66	65	ancoms 453	. . . . . . . . . . 11 $\$ $/\$ $\$ $\$ $\$
67	66	eqeq1d 2446	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
68	67	rexbidva 2727	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$
69	68	adantl 466	. . . . . . . 8 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
70	64, 69	bitrd 253	. . . . . . 7 $/\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
71	62, 70	mpbid 210	. . . . . 6 $/\$ $\$ $\$ $/\$ $\$ $\$
72	71	ralrimiva 2794	. . . . 5 $/\$ $\$ $\$ $\$ $\$
73	8, 72	jca 532	. . . 4 $/\$ $\$ $\$ $/\$ $\$ $\$
74		fvex 5696	. . . . . . . . 9
75	1, 74	eqeltri 2508	. . . . . . . 8
76	75	rnex 6507	. . . . . . 7
77	4, 76	eqeltri 2508	. . . . . 6
78		difexg 4435	. . . . . 6 $\$
79	77, 78	mp1i 12	. . . . 5 $/\$ $/\$ $\$ $\$ $\$
80		ffn 5554	. . . . . . . . 9
81	14, 80	syl 16	. . . . . . . 8
82	81	adantr 465	. . . . . . 7 $/\$ $/\$ $\$ $\$
83		fnssres 5519	. . . . . . 7 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
84	82, 13, 83	sylancl 662	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
85		ovres 6225	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
86	85	adantl 466	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
87		eldifi 3473	. . . . . . . . . . . 12 $\$
88		eldifi 3473	. . . . . . . . . . . 12 $\$
89	87, 88	anim12i 566	. . . . . . . . . . 11 $\$ $/\$ $\$ $/\$
90	1, 2, 4	rngocl 23820	. . . . . . . . . . . 12 $/\$ $/\$
91	90	3expb 1188	. . . . . . . . . . 11 $/\$ $/\$
92	89, 91	sylan2 474	. . . . . . . . . 10 $/\$ $\$ $/\$ $\$
93	92	adantlr 714	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
94		oveq2 6094	. . . . . . . . . . . . . . . 16
95	94	eqeq1d 2446	. . . . . . . . . . . . . . 15
96	95	rexbidv 2731	. . . . . . . . . . . . . 14 $\$ $\$
97	96	rspcv 3064	. . . . . . . . . . . . 13 $\$ $\$ $\$ $\$
98	97	imdistanri 691	. . . . . . . . . . . 12 $\$ $\$ $/\$ $\$ $\$ $/\$ $\$
99		eldifsn 3995	. . . . . . . . . . . . . . 15 $\$ $/\$
100		ssrexv 3412	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
101	11, 100	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 $\$
102	1, 2, 3, 4, 6	zerdivemp1x 28714	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
103	101, 102	syl3an3 1253	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
104	87, 103	syl3an2 1252	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $\$
105	104	3expb 1188	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$ $\$
106	105	imp 429	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $/\$
107	106	necon3d 2641	. . . . . . . . . . . . . . . 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 3995	. . . . . . . . 9 $\$ $/\$
116	93, 114, 115	sylanbrc 664	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$
117	86, 116	eqeltrd 2512	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
118	117	ralrimivva 2803	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
119		ffnov 6189	. . . . . 6 $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
120	84, 118, 119	sylanbrc 664	. . . . 5 $/\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
121	116	3adantr3 1149	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
122		simpr3 996	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
123	121, 122	ovresd 6226	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
124	85	3adant3 1008	. . . . . . . 8 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
125	124	adantl 466	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
126	125	oveq1d 6101	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
127		ovres 6225	. . . . . . . . . 10 $\$ $/\$ $\$ $\$ $\$
128	127	3adant1 1006	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
129	128	adantl 466	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
130	129	oveq2d 6102	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
131		simpr1 994	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
132		fovrn 6228	. . . . . . . . . 10 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
133	132	3adant3r1 1196	. . . . . . . . 9 $\$ $\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
134	120, 133	sylan 471	. . . . . . . 8 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
135	131, 134	ovresd 6226	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
136		eldifi 3473	. . . . . . . . . 10 $\$
137	87, 88, 136	3anim123i 1173	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
138	1, 2, 4	rngoass 23825	. . . . . . . . 9 $/\$ $/\$ $/\$
139	137, 138	sylan2 474	. . . . . . . 8 $/\$ $\$ $/\$ $\$ $/\$ $\$
140	139	adantlr 714	. . . . . . 7 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
141	130, 135, 140	3eqtr4d 2480	. . . . . 6 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$
142	123, 126, 141	3eqtr4d 2480	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$ $\$
143	44	anim1i 568	. . . . . . 7 $/\$ $/\$
144	143, 46	sylibr 212	. . . . . 6 $/\$ $\$
145	144	adantrr 716	. . . . 5 $/\$ $/\$ $\$ $\$ $\$
146		ovres 6225	. . . . . . . 8 $\$ $/\$ $\$ $\$ $\$
147	144, 146	sylan 471	. . . . . . 7 $/\$ $/\$ $\$ $\$ $\$
148	2, 43, 6	rngolidm 23862	. . . . . . . . 9 $/\$
149	87, 148	sylan2 474	. . . . . . . 8 $/\$ $\$
150	149	adantlr 714	. . . . . . 7 $/\$ $/\$ $\$
151	147, 150	eqtrd 2470	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$
152	151	adantlrr 720	. . . . 5 $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $\$
153	96	rspcva 3066	. . . . . . . . 9 $\$ $/\$ $\$ $\$ $\$
154		oveq1 6093	. . . . . . . . . . . 12
155	154	eqeq1d 2446	. . . . . . . . . . 11
156	155	cbvrexv 2943	. . . . . . . . . 10 $\$ $\$
157		ovres 6225	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
158	157	eqeq1d 2446	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $\$ $\$
159	158	ancoms 453	. . . . . . . . . . . 12 $\$ $/\$ $\$ $\$ $\$
160	159	rexbidva 2727	. . . . . . . . . . 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 23735	. . . 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 1369

wcel 1756

wne 2601

wral 2710

wrex 2711

cvv 2967 $\$ cdif 3320

cin 3322

wss 3323

csn 3872

cxp 4833

cdm 4835

crn 4836

cres 4837

wfn 5408

wf 5409

cfv 5413 (class class class)co 6086

c1st 6570

c2nd 6571

cgr 23624 GIdcgi 23625

cgn 23626

cexid 23752

cmagm 23756 MndOpcmndo 23775

crngo 23813

cdrng 23843

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-riota 6047 df-ov 6089 df-om 6472 df-1st 6572 df-2nd 6573 df-1o 6912 df-er 7093 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-grpo 23629 df-gid 23630 df-ginv 23631 df-ablo 23720 df-ass 23751 df-exid 23753 df-mgm 23757 df-sgr 23769 df-mndo 23776 df-rngo 23814 df-drngo 23844

This theorem is referenced by: isdrngo3 28718 divrngidl 28781

W3C validator