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

Theorem rngosn3 22006
 Description: The only unital ring with a base set consisting in one element is the zero ring. (Contributed by FL, 13-Feb-2010.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.)
Hypotheses
Ref Expression
on1el3.1
on1el3.2
Assertion
Ref Expression
rngosn3

Proof of Theorem rngosn3
StepHypRef Expression
1 on1el3.1 . . . . . . . . . 10
21rngogrpo 21970 . . . . . . . . 9
3 on1el3.2 . . . . . . . . . 10
43grpofo 21779 . . . . . . . . 9
5 fof 5645 . . . . . . . . 9
62, 4, 53syl 19 . . . . . . . 8
76adantr 452 . . . . . . 7
8 id 20 . . . . . . . . 9
98, 8xpeq12d 4895 . . . . . . . 8
109, 8feq23d 5580 . . . . . . 7
117, 10syl5ibcom 212 . . . . . 6
12 fdm 5587 . . . . . . . . . 10
137, 12syl 16 . . . . . . . . 9
1413eqcomd 2440 . . . . . . . 8
15 fdm 5587 . . . . . . . . 9
1615eqeq2d 2446 . . . . . . . 8
1714, 16syl5ibcom 212 . . . . . . 7
18 xpid11 5083 . . . . . . 7
1917, 18syl6ib 218 . . . . . 6
2011, 19impbid 184 . . . . 5
21 simpr 448 . . . . . . 7
22 xpsng 5901 . . . . . . 7
2321, 22sylancom 649 . . . . . 6
2423feq2d 5573 . . . . 5
25 opex 4419 . . . . . 6
26 fsng 5899 . . . . . 6
2725, 21, 26sylancr 645 . . . . 5
2820, 24, 273bitrd 271 . . . 4
291eqeq1i 2442 . . . 4
3028, 29syl6bb 253 . . 3
3130anbi1d 686 . 2
32 eqid 2435 . . . . . . 7
331, 32, 3rngosm 21961 . . . . . 6
3433adantr 452 . . . . 5
359, 8feq23d 5580 . . . . 5
3634, 35syl5ibcom 212 . . . 4
3723feq2d 5573 . . . . 5
38 fsng 5899 . . . . . 6
3925, 21, 38sylancr 645 . . . . 5
4037, 39bitrd 245 . . . 4
4136, 40sylibd 206 . . 3
4241pm4.71d 616 . 2
43 relrngo 21957 . . . . . 6
44 df-rel 4877 . . . . . 6
4543, 44mpbi 200 . . . . 5
4645sseli 3336 . . . 4