Theorem zrdivrng 10418

Description: The zero ring is not a division ring. (Contributed by FL, 24-Jan-2010.)

Hypothesis

Ref	Expression
zrdivrng.1	|- A e. B

Assertion

Ref	Expression
zrdivrng	|- -. <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. DivRing

Proof of Theorem zrdivrng

Step	Hyp	Ref	Expression
1		snex 3492	. 2 |- {<.<.A, A>., A>.} e. _V
2		0ngrp 9335	. . . . . 6 |- -. (/) e. Grp
3		opex 3527	. . . . . . . . . . . . . 14 |- <.A, A>. e. _V
4		zrdivrng.1	. . . . . . . . . . . . . . 15 |- A e. B
5	4	elisseti 2301	. . . . . . . . . . . . . 14 |- A e. _V
6	3, 5	rnsnop 4375	. . . . . . . . . . . . 13 |- ran {<.<.A, A>., A>.} = {A}
7	5	grpsn 9340	. . . . . . . . . . . . . 14 |- {<.<.A, A>., A>.} e. Grp
8	6	eqcomi 1888	. . . . . . . . . . . . . . . . 17 |- {A} = ran {<.<.A, A>., A>.}
9		eqid 1884	. . . . . . . . . . . . . . . . 17 |- (Id` {<.<.A, A>., A>.}) = (Id` {<.<.A, A>., A>.})
10	8, 9	grpidval 9342	. . . . . . . . . . . . . . . 16 |- ({<.<.A, A>., A>.} e. Grp -> (Id` {<.<.A, A>., A>.}) = U.{u e. {A} | A.x e. {A} (u{<.<.A, A>., A>.}x) = x})
11		elsni 3066	. . . . . . . . . . . . . . . . . . . . . 22 |- (u e. {A} -> u = A)
12	11	adantr 425	. . . . . . . . . . . . . . . . . . . . 21 |- ((u e. {A} /\ A.x e. {A} (u{<.<.A, A>., A>.}x) = x) -> u = A)
13		elsn 3058	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. {A} <-> u = A)
14	13	biimpri 169	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = A -> u e. {A})
15		elsn 3058	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. {A} <-> x = A)
16		df-fn 4009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ({<.<.A, A>., A>.} Fn ({A} X. {A}) <-> (Fun {<.<.A, A>., A>.} /\ dom {<.<.A, A>., A>.} = ({A} X. {A})))
17	3, 5	funsn 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- Fun {<.<.A, A>., A>.}
18		dmsnop 4367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- dom {<.<.A, A>., A>.} = {<.A, A>.}
19	5, 5	xpsn 4808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ({A} X. {A}) = {<.A, A>.}
20	18, 19	eqtr4i 1911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- dom {<.<.A, A>., A>.} = ({A} X. {A})
21	16, 17, 20	mpbir2an 800	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- {<.<.A, A>., A>.} Fn ({A} X. {A})
22	5	snid 3069	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- A e. {A}
23		opex 3527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- <.<.A, A>., A>. e. _V
24	23	snid 3069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- <.<.A, A>., A>. e. {<.<.A, A>., A>.}
25	5	fnotoprb 4916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (({<.<.A, A>., A>.} Fn ({A} X. {A}) /\ A e. {A} /\ A e. {A}) -> ((A{<.<.A, A>., A>.}A) = A <-> <.<.A, A>., A>. e. {<.<.A, A>., A>.}))
26	24, 25	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (({<.<.A, A>., A>.} Fn ({A} X. {A}) /\ A e. {A} /\ A e. {A}) -> (A{<.<.A, A>., A>.}A) = A)
27	21, 22, 22, 26	mp3an 1191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A{<.<.A, A>., A>.}A) = A
28		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((x = A /\ u = A) -> u = A)
29	28	opreq1d 4897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((x = A /\ u = A) -> (u{<.<.A, A>., A>.}x) = (A{<.<.A, A>., A>.}x))
30	29	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x = A /\ u = A) -> ((u{<.<.A, A>., A>.}x) = x <-> (A{<.<.A, A>., A>.}x) = x))
31		simpl 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((x = A /\ u = A) -> x = A)
32	31	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((x = A /\ u = A) -> (A{<.<.A, A>., A>.}x) = (A{<.<.A, A>., A>.}A))
33	32, 31	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x = A /\ u = A) -> ((A{<.<.A, A>., A>.}x) = x <-> (A{<.<.A, A>., A>.}A) = A))
34	30, 33	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x = A /\ u = A) -> ((u{<.<.A, A>., A>.}x) = x <-> (A{<.<.A, A>., A>.}A) = A))
35	27, 34	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x = A /\ u = A) -> (u{<.<.A, A>., A>.}x) = x)
36	35	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x = A -> (u = A -> (u{<.<.A, A>., A>.}x) = x))
37	15, 36	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. {A} -> (u = A -> (u{<.<.A, A>., A>.}x) = x))
38	37	com12 14	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u = A -> (x e. {A} -> (u{<.<.A, A>., A>.}x) = x))
39	38	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = A -> A.x e. {A} (u{<.<.A, A>., A>.}x) = x)
40	14, 39	jca 310	. . . . . . . . . . . . . . . . . . . . 21 |- (u = A -> (u e. {A} /\ A.x e. {A} (u{<.<.A, A>., A>.}x) = x))
41	12, 40	impbii 174	. . . . . . . . . . . . . . . . . . . 20 |- ((u e. {A} /\ A.x e. {A} (u{<.<.A, A>., A>.}x) = x) <-> u = A)
42	41	abbii 2006	. . . . . . . . . . . . . . . . . . 19 |- {u | (u e. {A} /\ A.x e. {A} (u{<.<.A, A>., A>.}x) = x)} = {u | u = A}
43		df-rab 2112	. . . . . . . . . . . . . . . . . . 19 |- {u e. {A} | A.x e. {A} (u{<.<.A, A>., A>.}x) = x} = {u | (u e. {A} /\ A.x e. {A} (u{<.<.A, A>., A>.}x) = x)}
44		df-sn 3049	. . . . . . . . . . . . . . . . . . 19 |- {A} = {u | u = A}
45	42, 43, 44	3eqtr4i 1921	. . . . . . . . . . . . . . . . . 18 |- {u e. {A} | A.x e. {A} (u{<.<.A, A>., A>.}x) = x} = {A}
46	45	unieqi 3187	. . . . . . . . . . . . . . . . 17 |- U.{u e. {A} | A.x e. {A} (u{<.<.A, A>., A>.}x) = x} = U.{A}
47	5	unisn 3193	. . . . . . . . . . . . . . . . 17 |- U.{A} = A
48	46, 47	eqtri 1908	. . . . . . . . . . . . . . . 16 |- U.{u e. {A} | A.x e. {A} (u{<.<.A, A>., A>.}x) = x} = A
49	10, 48	syl6eq 1944	. . . . . . . . . . . . . . 15 |- ({<.<.A, A>., A>.} e. Grp -> (Id` {<.<.A, A>., A>.}) = A)
50	49	sneqd 3056	. . . . . . . . . . . . . 14 |- ({<.<.A, A>., A>.} e. Grp -> {(Id` {<.<.A, A>., A>.})} = {A})
51	7, 50	ax-mp 7	. . . . . . . . . . . . 13 |- {(Id` {<.<.A, A>., A>.})} = {A}
52	6, 51	difeq12i 2724	. . . . . . . . . . . 12 |- (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) = ({A} \ {A})
53		difid 2942	. . . . . . . . . . . 12 |- ({A} \ {A}) = (/)
54	52, 53	eqtri 1908	. . . . . . . . . . 11 |- (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) = (/)
55	54	xpeq1i 4021	. . . . . . . . . 10 |- ((ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})})) = ((/) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}))
56		xp0r 4065	. . . . . . . . . 10 |- ((/) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})})) = (/)
57	55, 56	eqtri 1908	. . . . . . . . 9 |- ((ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})})) = (/)
58		reseq2 4219	. . . . . . . . 9 |- (((ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})})) = (/) -> ({<.<.A, A>., A>.} |` ((ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}))) = ({<.<.A, A>., A>.} |` (/)))
59	57, 58	ax-mp 7	. . . . . . . 8 |- ({<.<.A, A>., A>.} |` ((ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}))) = ({<.<.A, A>., A>.} |` (/))
60		res0 4221	. . . . . . . 8 |- ({<.<.A, A>., A>.} |` (/)) = (/)
61	59, 60	eqtri 1908	. . . . . . 7 |- ({<.<.A, A>., A>.} |` ((ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}))) = (/)
62	61	eleq1i 1960	. . . . . 6 |- (({<.<.A, A>., A>.} |` ((ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}))) e. Grp <-> (/) e. Grp)
63	2, 62	mtbir 209	. . . . 5 |- -. ({<.<.A, A>., A>.} |` ((ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}))) e. Grp
64	63	a1i 8	. . . 4 |- ({<.<.A, A>., A>.} e. _V -> -. ({<.<.A, A>., A>.} |` ((ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}))) e. Grp)
65	64	intnand 757	. . 3 |- ({<.<.A, A>., A>.} e. _V -> -. (<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. Ring /\ ({<.<.A, A>., A>.} |` ((ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}))) e. Grp))
66		isdivrng 10417	. . 3 |- ({<.<.A, A>., A>.} e. _V -> (<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. DivRing <-> (<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. Ring /\ ({<.<.A, A>., A>.} |` ((ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}) X. (ran {<.<.A, A>., A>.} \ {(Id` {<.<.A, A>., A>.})}))) e. Grp)))
67	65, 66	mtbird 783	. 2 |- ({<.<.A, A>., A>.} e. _V -> -. <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. DivRing)
68	1, 67	ax-mp 7	1 |- -. <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. DivRing

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  {cab 1871  A.wral 2105  {crab 2108  _Vcvv 2292   \ cdif 2590  (/)c0 2875  {csn 3044  <.cop 3046  U.cuni 3177   X. cxp 3984  dom cdm 3986  ran crn 3987   |` cres 3988  Fun wfun 3992   Fn wfn 3993  ` cfv 3998  (class class class)co 4884  Grpcgr 9311  Idcgi 9312  Ringcring 9463  DivRingcdrng 9491

This theorem is referenced by:  dvrunz 10419  zrfld 14784

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-1st 5020  df-2nd 5021  df-grp 9316  df-gid 9317  df-ring 9464  df-drng 9492

Copyright terms: Public domain