Theorem ringsn 8159

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 2756	. . 3 |- {<.<.A, A>., A>.} e. V
2		opex 2788	. . . . . 6 |- <.A, A>. e. V
3		ringsn.1	. . . . . 6 |- A e. V
4	2, 3	rnsnop 3456	. . . . 5 |- ran {<.<.A, A>., A>.} = {A}
5	4	eqcomi 1482	. . . 4 |- {A} = ran {<.<.A, A>., A>.}
6	5	isring 8137	. . 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 8121	. . 3 |- {<.<.A, A>., A>.} e. Abel
9		ffnoprval 4020	. . . 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 3199	. . . . 5 |- ({<.<.A, A>., A>.} Fn ({A} X. {A}) <-> (Fun {<.<.A, A>., A>.} /\ dom {<.<.A, A>., A>.} = ({A} X. {A})))
11	2, 3	funsn 3549	. . . . 5 |- Fun {<.<.A, A>., A>.}
12		dmsnop 3334	. . . . . 6 |- dom {<.<.A, A>., A>.} = {<.A, A>.}
13	3, 3	xpsn 3841	. . . . . 6 |- ({A} X. {A}) = {<.A, A>.}
14	12, 13	eqtr4 1501	. . . . 5 |- dom {<.<.A, A>., A>.} = ({A} X. {A})
15	10, 11, 14	mpbir2an 732	. . . 4 |- {<.<.A, A>., A>.} Fn ({A} X. {A})
16		opreq12 3976	. . . . . . . 8 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) = (A{<.<.A, A>., A>.}A))
17		df-opr 3971	. . . . . . . . 9 |- (A{<.<.A, A>., A>.}A) = ({<.<.A, A>., A>.}` <.A, A>.)
18	2, 3	fvsn 3800	. . . . . . . . 9 |- ({<.<.A, A>., A>.}` <.A, A>.) = A
19	17, 18	eqtr 1498	. . . . . . . 8 |- (A{<.<.A, A>., A>.}A) = A
20	16, 19	syl6eq 1526	. . . . . . 7 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) = A)
21	3	elsnc2 2441	. . . . . . 7 |- ((x{<.<.A, A>., A>.}y) e. {A} <-> (x{<.<.A, A>., A>.}y) = A)
22	20, 21	sylibr 200	. . . . . 6 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) e. {A})
23		elsn 2425	. . . . . 6 |- (x e. {A} <-> x = A)
24		elsn 2425	. . . . . 6 |- (y e. {A} <-> y = A)
25	22, 23, 24	syl2anb 457	. . . . 5 |- ((x e. {A} /\ y e. {A}) -> (x{<.<.A, A>., A>.}y) e. {A})
26	25	rgen2a 1702	. . . 4 |- A.x e. {A}A.y e. {A} (x{<.<.A, A>., A>.}y) e. {A}
27	9, 15, 26	mpbir2an 732	. . 3 |- {<.<.A, A>., A>.}:({A} X. {A})-->{A}
28	8, 27	pm3.2i 285	. 2 |- ({<.<.A, A>., A>.} e. Abel /\ {<.<.A, A>., A>.}:({A} X. {A})-->{A})
29		pm3.26 319	. . . . . . . . 9 |- ((x = A /\ y = A) -> x = A)
30	19, 16, 29	3eqtr4a 1535	. . . . . . . 8 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) = x)
31	30	3adant3 801	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> (x{<.<.A, A>., A>.}y) = x)
32		pm3.27 323	. . . . . . . . 9 |- ((y = A /\ z = A) -> z = A)
33		opreq12 3976	. . . . . . . . . 10 |- ((y = A /\ z = A) -> (y{<.<.A, A>., A>.}z) = (A{<.<.A, A>., A>.}A))
34	33, 19	syl6eq 1526	. . . . . . . . 9 |- ((y = A /\ z = A) -> (y{<.<.A, A>., A>.}z) = A)
35	32, 34	eqtr4d 1513	. . . . . . . 8 |- ((y = A /\ z = A) -> z = (y{<.<.A, A>., A>.}z))
36	35	3adant1 799	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> z = (y{<.<.A, A>., A>.}z))
37	31, 36	opreq12d 3984	. . . . . 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 1513	. . . . . . . 8 |- ((x = A /\ y = A) -> x = (x{<.<.A, A>., A>.}y))
39	38	3adant3 801	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> x = (x{<.<.A, A>., A>.}y))
40		eqtr3t 1497	. . . . . . . . . 10 |- ((y = A /\ x = A) -> y = x)
41	40	opreq1d 3981	. . . . . . . . 9 |- ((y = A /\ x = A) -> (y{<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.}z))
42	41	ancoms 438	. . . . . . . 8 |- ((x = A /\ y = A) -> (y{<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.}z))
43	42	3adant3 801	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> (y{<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.}z))
44	39, 43	opreq12d 3984	. . . . . 6 |- ((x = A /\ y = A /\ z = A) -> (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = ((x{<.<.A, A