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

Theorem rngosn3 25554
 Description: Obsolete as of 25-Jan-2020. Use ring1zr 18049 or srg1zr 17306 instead. 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 25518 . . . . . . . . 9
3 on1el3.2 . . . . . . . . . 10
43grpofo 25327 . . . . . . . . 9
5 fof 5801 . . . . . . . . 9
62, 4, 53syl 20 . . . . . . . 8
76adantr 465 . . . . . . 7
8 id 22 . . . . . . . . 9
98sqxpeqd 5034 . . . . . . . 8
109, 8feq23d 5732 . . . . . . 7
117, 10syl5ibcom 220 . . . . . 6
12 fdm 5741 . . . . . . . . . 10
137, 12syl 16 . . . . . . . . 9
1413eqcomd 2465 . . . . . . . 8
15 fdm 5741 . . . . . . . . 9
1615eqeq2d 2471 . . . . . . . 8
1714, 16syl5ibcom 220 . . . . . . 7
18 xpid11 5234 . . . . . . 7
1917, 18syl6ib 226 . . . . . 6
2011, 19impbid 191 . . . . 5
21 simpr 461 . . . . . . 7
22 xpsng 6073 . . . . . . 7
2321, 22sylancom 667 . . . . . 6
2423feq2d 5724 . . . . 5
25 opex 4720 . . . . . 6
26 fsng 6071 . . . . . 6
2725, 21, 26sylancr 663 . . . . 5
2820, 24, 273bitrd 279 . . . 4
291eqeq1i 2464 . . . 4
3028, 29syl6bb 261 . . 3
3130anbi1d 704 . 2
32 eqid 2457 . . . . . . 7
331, 32, 3rngosm 25509 . . . . . 6
3433adantr 465 . . . . 5
359, 8feq23d 5732 . . . . 5
3634, 35syl5ibcom 220 . . . 4
3723feq2d 5724 . . . . 5
38 fsng 6071 . . . . . 6
3925, 21, 38sylancr 663 . . . . 5
4037, 39bitrd 253 . . . 4
4136, 40sylibd 214 . . 3
4241pm4.71d 634 . 2
43 relrngo 25505 . . . . . 6
44 df-rel 5015 . . . . . 6
4543, 44mpbi 208 . . . . 5
4645sseli 3495 . . . 4