Theorem ringsn 9490

Description: The trivial or zero ring defined on a singleton set {A} (see http://en.wikipedia.org/wiki/Trivial_ring). (Contributed by Steve Rodriguez, 10-Feb-2007.)

Hypothesis

Ref	Expression
ringsn.1	|- A e. _V

Assertion

Ref	Expression
ringsn	|- <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. Ring

Proof of Theorem ringsn

Step	Hyp	Ref	Expression
1		snex 3492	. . 3 |- {<.<.A, A>., A>.} e. _V
2		opex 3527	. . . . . 6 |- <.A, A>. e. _V
3		ringsn.1	. . . . . 6 |- A e. _V
4	2, 3	rnsnop 4375	. . . . 5 |- ran {<.<.A, A>., A>.} = {A}
5	4	eqcomi 1888	. . . 4 |- {A} = ran {<.<.A, A>., A>.}
6	5	isring 9465	. . 3 |- ({<.<.A, A>., A>.} e. _V -> (<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. Ring <-> (({<.<.A, A>., A>.} e. Abel /\ {<.<.A, A>., A>.}:({A} X. {A})-->{A}) /\ (A.x e. {A}A.y e. {A}A.z e. {A} (((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) /\ (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.} (x{<.<.A, A>., A>.}z)) /\ ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = ((x{<.<.A, A>., A>.}z){<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z))) /\ E.x e. {A}A.y e. {A} ((y{<.<.A, A>., A>.}x) = y /\ (x{<.<.A, A>., A>.}y) = y)))))
7	1, 6	ax-mp 7	. 2 |- (<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. Ring <-> (({<.<.A, A>., A>.} e. Abel /\ {<.<.A, A>., A>.}:({A} X. {A})-->{A}) /\ (A.x e. {A}A.y e. {A}A.z e. {A} (((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) /\ (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.} (x{<.<.A, A>., A>.}z)) /\ ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = ((x{<.<.A, A>., A>.}z){<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z))) /\ E.x e. {A}A.y e. {A} ((y{<.<.A, A>., A>.}x) = y /\ (x{<.<.A, A>., A>.}y) = y))))
8	3	ablsn 9433	. . 3 |- {<.<.A, A>., A>.} e. Abel
9		ffnoprv 4943	. . . 4 |- ({<.<.A, A>., A>.}:({A} X. {A})-->{A} <-> ({<.<.A, A>., A>.} Fn ({A} X. {A}) /\ A.x e. {A}A.y e. {A} (x{<.<.A, A>., A>.}y) e. {A}))
10		df-fn 4009	. . . . 5 |- ({<.<.A, A>., A>.} Fn ({A} X. {A}) <-> (Fun {<.<.A, A>., A>.} /\ dom {<.<.A, A>., A>.} = ({A} X. {A})))
11	2, 3	funsn 4463	. . . . 5 |- Fun {<.<.A, A>., A>.}
12		dmsnop 4367	. . . . . 6 |- dom {<.<.A, A>., A>.} = {<.A, A>.}
13	3, 3	xpsn 4808	. . . . . 6 |- ({A} X. {A}) = {<.A, A>.}
14	12, 13	eqtr4i 1911	. . . . 5 |- dom {<.<.A, A>., A>.} = ({A} X. {A})
15	10, 11, 14	mpbir2an 800	. . . 4 |- {<.<.A, A>., A>.} Fn ({A} X. {A})
16		opreq12 4891	. . . . . . . 8 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) = (A{<.<.A, A>., A>.}A))
17		df-opr 4886	. . . . . . . . 9 |- (A{<.<.A, A>., A>.}A) = ({<.<.A, A>., A>.}` <.A, A>.)
18	2, 3	fvsn 4758	. . . . . . . . 9 |- ({<.<.A, A>., A>.}` <.A, A>.) = A
19	17, 18	eqtri 1908	. . . . . . . 8 |- (A{<.<.A, A>., A>.}A) = A
20	16, 19	syl6eq 1944	. . . . . . 7 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) = A)
21	3	elsnc2 3071	. . . . . . 7 |- ((x{<.<.A, A>., A>.}y) e. {A} <-> (x{<.<.A, A>., A>.}y) = A)
22	20, 21	sylibr 217	. . . . . 6 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) e. {A})
23		elsn 3058	. . . . . 6 |- (x e. {A} <-> x = A)
24		elsn 3058	. . . . . 6 |- (y e. {A} <-> y = A)
25	22, 23, 24	syl2anb 504	. . . . 5 |- ((x e. {A} /\ y e. {A}) -> (x{<.<.A, A>., A>.}y) e. {A})
26	25	rgen2a 2160	. . . 4 |- A.x e. {A}A.y e. {A} (x{<.<.A, A>., A>.}y) e. {A}
27	9, 15, 26	mpbir2an 800	. . 3 |- {<.<.A, A>., A>.}:({A} X. {A})-->{A}
28	8, 27	pm3.2i 307	. 2 |- ({<.<.A, A>., A>.} e. Abel /\ {<.<.A, A>., A>.}:({A} X. {A})-->{A})
29		simpl 346	. . . . . . . . 9 |- ((x = A /\ y = A) -> x = A)
30	19, 16, 29	3eqtr4a 1954	. . . . . . . 8 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) = x)
31	30	3adant3 896	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> (x{<.<.A, A>., A>.}y) = x)
32		simpr 350	. . . . . . . . 9 |- ((y = A /\ z = A) -> z = A)
33		opreq12 4891	. . . . . . . . . 10 |- ((y = A /\ z = A) -> (y{<.<.A, A>., A>.}z) = (A{<.<.A, A>., A>.}A))
34	33, 19	syl6eq 1944	. . . . . . . . 9 |- ((y = A /\ z = A) -> (y{<.<.A, A>., A>.}z) = A)
35	32, 34	eqtr4d 1928	. . . . . . . 8 |- ((y = A /\ z = A) -> z = (y{<.<.A, A>., A>.}z))
36	35	3adant1 894	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> z = (y{<.<.A, A>., A>.}z))
37	31, 36	opreq12d 4900	. . . . . 6 |- ((x = A /\ y = A /\ z = A) -> ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)))
38	29, 20	eqtr4d 1928	. . . . . . . 8 |- ((x = A /\ y = A) -> x = (x{<.<.A, A>., A>.}y))
39	38	3adant3 896	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> x = (x{<.<.A, A>., A>.}y))
40		eqtr3 1907	. . . . . . . . . 10 |- ((y = A /\ x = A) -> y = x)
41	40	opreq1d 4897	. . . . . . . . 9 |- ((y = A /\ x = A) -> (y{<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.}z))
42	41	ancoms 484	. . . . . . . 8 |- ((x = A /\ y = A) -> (y{<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.}z))
43	42	3adant3 896	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> (y{<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.}z))
44	39, 43	opreq12d 4900	. . . . . 6 |- ((x = A /\ y = A /\ z = A) -> (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.} (x{<.<.A, A>., A>.}z)))
45		eqtr3 1907	. . . . . . . . 9 |- ((y = A /\ z = A) -> y = z)
46	45	opreq2d 4898	. . . . . . . 8 |- ((y = A /\ z = A) -> (x{<.<.A, A>., A>.}y) = (x{<.<.A, A>., A>.}z))
47	46	3adant1 894	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> (x{<.<.A, A>., A>.}y) = (x{<.<.A, A>., A>.}z))
48	47, 36	opreq12d 4900	. . . . . 6 |- ((x = A /\ y = A /\ z = A) -> ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = ((x{<.<.A, A>., A>.}z){<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)))
49	37, 44, 48	3jca 1050	. . . . 5 |- ((x = A /\ y = A /\ z = A) -> (((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) /\ (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.} (x{<.<.A, A>., A>.}z)) /\ ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = ((x{<.<.A, A>., A>.}z){<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z))))
50		elsn 3058	. . . . 5 |- (z e. {A} <-> z = A)
51	49, 23, 24, 50	syl3anb 1140	. . . 4 |- ((x e. {A} /\ y e. {A} /\ z e. {A}) -> (((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) /\ (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.} (x{<.<.A, A>., A>.}z)) /\ ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = ((x{<.<.A, A>., A>.}z){<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z))))
52	51	rgen3 2187	. . 3 |- A.x e. {A}A.y e. {A}A.z e. {A} (((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) /\ (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.} (x{<.<.A, A>., A>.}z)) /\ ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = ((x{<.<.A, A>., A>.}z){<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)))
53	3	snid 3069	. . . 4 |- A e. {A}
54	19, 19	pm3.2i 307	. . . . . . 7 |- ((A{<.<.A, A>., A>.}A) = A /\ (A{<.<.A, A>., A>.}A) = A)
55		opreq1 4889	. . . . . . . . 9 |- (y = A -> (y{<.<.A, A>., A>.}A) = (A{<.<.A, A>., A>.}A))
56		id 73	. . . . . . . . 9 |- (y = A -> y = A)
57	55, 56	eqeq12d 1899	. . . . . . . 8 |- (y = A -> ((y{<.<.A, A>., A>.}A) = y <-> (A{<.<.A, A>., A>.}A) = A))
58		opreq2 4890	. . . . . . . . 9 |- (y = A -> (A{<.<.A, A>., A>.}y) = (A{<.<.A, A>., A>.}A))
59	58, 56	eqeq12d 1899	. . . . . . . 8 |- (y = A -> ((A{<.<.A, A>., A>.}y) = y <-> (A{<.<.A, A>., A>.}A) = A))
60	57, 59	anbi12d 690	. . . . . . 7 |- (y = A -> (((y{<.<.A, A>., A>.}A) = y /\ (A{<.<.A, A>., A>.}y) = y) <-> ((A{<.<.A, A>., A>.}A) = A /\ (A{<.<.A, A>., A>.}A) = A)))
61	54, 60	mpbiri 211	. . . . . 6 |- (y = A -> ((y{<.<.A, A>., A>.}A) = y /\ (A{<.<.A, A>., A>.}y) = y))
62	24, 61	sylbi 216	. . . . 5 |- (y e. {A} -> ((y{<.<.A, A>., A>.}A) = y /\ (A{<.<.A, A>., A>.}y) = y))
63	62	rgen 2159	. . . 4 |- A.y e. {A} ((y{<.<.A, A>., A>.}A) = y /\ (A{<.<.A, A>., A>.}y) = y)
64		opreq2 4890	. . . . . . . 8 |- (x = A -> (y{<.<.A, A>., A>.}x) = (y{<.<.A, A>., A>.}A))
65	64	eqeq1d 1892	. . . . . . 7 |- (x = A -> ((y{<.<.A, A>., A>.}x) = y <-> (y{<.<.A, A>., A>.}A) = y))
66		opreq1 4889	. . . . . . . 8 |- (x = A -> (x{<.<.A, A>., A>.}y) = (A{<.<.A, A>., A>.}y))
67	66	eqeq1d 1892	. . . . . . 7 |- (x = A -> ((x{<.<.A, A>., A>.}y) = y <-> (A{<.<.A, A>., A>.}y) = y))
68	65, 67	anbi12d 690	. . . . . 6 |- (x = A -> (((y{<.<.A, A>., A>.}x) = y /\ (x{<.<.A, A>., A>.}y) = y) <-> ((y{<.<.A, A>., A>.}A) = y /\ (A{<.<.A, A>., A>.}y) = y)))
69	68	ralbidv 2123	. . . . 5 |- (x = A -> (A.y e. {A} ((y{<.<.A, A>., A>.}x) = y /\ (x{<.<.A, A>., A>.}y) = y) <-> A.y e. {A} ((y{<.<.A, A>., A>.}A) = y /\ (A{<.<.A, A>., A>.}y) = y)))
70	69	rcla4ev 2381	. . . 4 |- ((A e. {A} /\ A.y e. {A} ((y{<.<.A, A>., A>.}A) = y /\ (A{<.<.A, A>., A>.}y) = y)) -> E.x e. {A}A.y e. {A} ((y{<.<.A, A>., A>.}x) = y /\ (x{<.<.A, A>., A>.}y) = y))
71	53, 63, 70	mp2an 761	. . 3 |- E.x e. {A}A.y e. {A} ((y{<.<.A, A>., A>.}x) = y /\ (x{<.<.A, A>., A>.}y) = y)
72	52, 71	pm3.2i 307	. 2 |- (A.x e. {A}A.y e. {A}A.z e. {A} (((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) /\ (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.} (x{<.<.A, A>., A>.}z)) /\ ((x{<.<.A, A>., A>.}y){<.<.A, A>., A>.}z) = ((x{<.<.A, A>., A>.}z){<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z))) /\ E.x e. {A}A.y e. {A} ((y{<.<.A, A>., A>.}x) = y /\ (x{<.<.A, A>., A>.}y) = y))
73	7, 28, 72	mpbir2an 800	1 |- <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>. e. Ring

Syntax hints:   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  _Vcvv 2292  {csn 3044  <.cop 3046   X. cxp 3984  dom cdm 3986  ran crn 3987  Fun wfun 3992   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  Abelcabl 9407  Ringcring 9463

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-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  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-grp 9316  df-abl 9408  df-ring 9464

Copyright terms: Public domain