Theorem ringsn 8115

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 2745	. . 3 |- {<.<.A, A>., A>.} e. V
2		opex 2777	. . . . . 6 |- <.A, A>. e. V
3		ringsn.1	. . . . . 6 |- A e. V
4	2, 3	rnsnop 3442	. . . . 5 |- ran {<.<.A, A>., A>.} = {A}
5	4	eqcomi 1476	. . . 4 |- {A} = ran {<.<.A, A>., A>.}
6	5	isring 8093	. . 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 8077	. . 3 |- {<.<.A, A>., A>.} e. Abel
9		ffnoprval 4005	. . . 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 3188	. . . . 5 |- ({<.<.A, A>., A>.} Fn ({A} X. {A}) <-> (Fun {<.<.A, A>., A>.} /\ dom {<.<.A, A>., A>.} = ({A} X. {A})))
11	2, 3	funsn 3535	. . . . 5 |- Fun {<.<.A, A>., A>.}
12		dmsnop 3323	. . . . . 6 |- dom {<.<.A, A>., A>.} = {<.A, A>.}
13	3, 3	xpsn 3826	. . . . . 6 |- ({A} X. {A}) = {<.A, A>.}
14	12, 13	eqtr4 1495	. . . . 5 |- dom {<.<.A, A>., A>.} = ({A} X. {A})
15	10, 11, 14	mpbir2an 729	. . . 4 |- {<.<.A, A>., A>.} Fn ({A} X. {A})
16		opreq12 3961	. . . . . . . 8 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) = (A{<.<.A, A>., A>.}A))
17		df-opr 3956	. . . . . . . . 9 |- (A{<.<.A, A>., A>.}A) = ({<.<.A, A>., A>.}` <.A, A>.)
18	2, 3	fvsn 3785	. . . . . . . . 9 |- ({<.<.A, A>., A>.}` <.A, A>.) = A
19	17, 18	eqtr 1492	. . . . . . . 8 |- (A{<.<.A, A>., A>.}A) = A
20	16, 19	syl6eq 1520	. . . . . . 7 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) = A)
21	3	elsnc2 2433	. . . . . . 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 2417	. . . . . 6 |- (x e. {A} <-> x = A)
24		elsn 2417	. . . . . 6 |- (y e. {A} <-> y = A)
25	22, 23, 24	syl2anb 455	. . . . 5 |- ((x e. {A} /\ y e. {A}) -> (x{<.<.A, A>., A>.}y) e. {A})
26	25	rgen2a 1696	. . . 4 |- A.x e. {A}A.y e. {A} (x{<.<.A, A>., A>.}y) e. {A}
27	9, 15, 26	mpbir2an 729	. . 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 1529	. . . . . . . 8 |- ((x = A /\ y = A) -> (x{<.<.A, A>., A>.}y) = x)
31	30	3adant3 798	. . . . . . 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 3961	. . . . . . . . . 10 |- ((y = A /\ z = A) -> (y{<.<.A, A>., A>.}z) = (A{<.<.A, A>., A>.}A))
34	33, 19	syl6eq 1520	. . . . . . . . 9 |- ((y = A /\ z = A) -> (y{<.<.A, A>., A>.}z) = A)
35	32, 34	eqtr4d 1507	. . . . . . . 8 |- ((y = A /\ z = A) -> z = (y{<.<.A, A>., A>.}z))
36	35	3adant1 796	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> z = (y{<.<.A, A>., A>.}z))
37	31, 36	opreq12d 3969	. . . . . 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 1507	. . . . . . . 8 |- ((x = A /\ y = A) -> x = (x{<.<.A, A>., A>.}y))
39	38	3adant3 798	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> x = (x{<.<.A, A>., A>.}y))
40		eqtr3t 1491	. . . . . . . . . 10 |- ((y = A /\ x = A) -> y = x)
41	40	opreq1d 3966	. . . . . . . . 9 |- ((y = A /\ x = A) -> (y{<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.}z))
42	41	ancoms 436	. . . . . . . 8 |- ((x = A /\ y = A) -> (y{<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.}z))
43	42	3adant3 798	. . . . . . 7 |- ((x = A /\ y = A /\ z = A) -> (y{<.<.A, A>., A>.}z) = (x{<.<.A, A>., A>.}z))
44	39, 43	opreq12d 3969	. . . . . 6 |- ((x = A /\ y = A /\ z = A) -> (x{<.<.A, A>., A>.} (y{<.<.A, A>., A>.}z)) = ((x{<.<.A, A>.,