Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rngosn Structured version   Unicode version

Theorem rngosn 21994
 Description: The trivial or zero ring defined on a singleton set (see http://en.wikipedia.org/wiki/Trivial_ring). (Contributed by Steve Rodriguez, 10-Feb-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
Hypothesis
Ref Expression
ringsn.1
Assertion
Ref Expression
rngosn

Proof of Theorem rngosn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ringsn.1 . . . . 5
21ablosn 21937 . . . 4
32a1i 11 . . 3
4 opex 4429 . . . . . 6
54rnsnop 5352 . . . . 5
65eqcomi 2442 . . . 4
76a1i 11 . . 3
8 ablogrpo 21874 . . . 4
96grpofo 21789 . . . 4
10 fof 5655 . . . 4
113, 8, 9, 104syl 20 . . 3
12 elsni 3840 . . . . . 6
13 elsni 3840 . . . . . 6
14 elsni 3840 . . . . . 6
1512, 13, 143anim123i 1140 . . . . 5
1615adantl 454 . . . 4
17 simp1 958 . . . . . . . 8
18 simp2 959 . . . . . . . 8
1917, 18oveq12d 6101 . . . . . . 7
20 df-ov 6086 . . . . . . . 8
214, 1fvsn 5928 . . . . . . . 8
2220, 21eqtri 2458 . . . . . . 7
2319, 22syl6eq 2486 . . . . . 6
2423, 17eqtr4d 2473 . . . . 5
25 simp3 960 . . . . . 6
2618, 25oveq12d 6101 . . . . . . 7
2726, 22syl6eq 2486 . . . . . 6
2825, 27eqtr4d 2473 . . . . 5
2924, 28oveq12d 6101 . . . 4
3016, 29syl 16 . . 3
3117, 23eqtr4d 2473 . . . . 5
3218, 17eqtr4d 2473 . . . . . 6
3332oveq1d 6098 . . . . 5
3431, 33oveq12d 6101 . . . 4
3516, 34syl 16 . . 3
3618, 25eqtr4d 2473 . . . . . 6
3736oveq2d 6099 . . . . 5
3837, 28oveq12d 6101 . . . 4
3916, 38syl 16 . . 3
401snid 3843 . . . 4
4140a1i 11 . . 3
4213oveq2d 6099 . . . . . 6
4342, 22syl6eq 2486 . . . . 5
4443, 13eqtr4d 2473 . . . 4