Metamath Proof Explorer


Theorem rngosn3

Description: Obsolete as of 25-Jan-2020. Use ring1zr or srg1zr 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.)

Ref Expression
Hypotheses on1el3.1 G = 1 st R
on1el3.2 X = ran G
Assertion rngosn3 R RingOps A B X = A R = A A A A A A

Proof

Step Hyp Ref Expression
1 on1el3.1 G = 1 st R
2 on1el3.2 X = ran G
3 1 rngogrpo R RingOps G GrpOp
4 2 grpofo G GrpOp G : X × X onto X
5 fof G : X × X onto X G : X × X X
6 3 4 5 3syl R RingOps G : X × X X
7 6 adantr R RingOps A B G : X × X X
8 id X = A X = A
9 8 sqxpeqd X = A X × X = A × A
10 9 8 feq23d X = A G : X × X X G : A × A A
11 7 10 syl5ibcom R RingOps A B X = A G : A × A A
12 7 fdmd R RingOps A B dom G = X × X
13 12 eqcomd R RingOps A B X × X = dom G
14 fdm G : A × A A dom G = A × A
15 14 eqeq2d G : A × A A X × X = dom G X × X = A × A
16 13 15 syl5ibcom R RingOps A B G : A × A A X × X = A × A
17 xpid11 X × X = A × A X = A
18 16 17 syl6ib R RingOps A B G : A × A A X = A
19 11 18 impbid R RingOps A B X = A G : A × A A
20 simpr R RingOps A B A B
21 xpsng A B A B A × A = A A
22 20 21 sylancom R RingOps A B A × A = A A
23 22 feq2d R RingOps A B G : A × A A G : A A A
24 opex A A V
25 fsng A A V A B G : A A A G = A A A
26 24 20 25 sylancr R RingOps A B G : A A A G = A A A
27 19 23 26 3bitrd R RingOps A B X = A G = A A A
28 1 eqeq1i G = A A A 1 st R = A A A
29 27 28 bitrdi R RingOps A B X = A 1 st R = A A A
30 29 anbi1d R RingOps A B X = A 2 nd R = A A A 1 st R = A A A 2 nd R = A A A
31 eqid 2 nd R = 2 nd R
32 1 31 2 rngosm R RingOps 2 nd R : X × X X
33 32 adantr R RingOps A B 2 nd R : X × X X
34 9 8 feq23d X = A 2 nd R : X × X X 2 nd R : A × A A
35 33 34 syl5ibcom R RingOps A B X = A 2 nd R : A × A A
36 22 feq2d R RingOps A B 2 nd R : A × A A 2 nd R : A A A
37 fsng A A V A B 2 nd R : A A A 2 nd R = A A A
38 24 20 37 sylancr R RingOps A B 2 nd R : A A A 2 nd R = A A A
39 36 38 bitrd R RingOps A B 2 nd R : A × A A 2 nd R = A A A
40 35 39 sylibd R RingOps A B X = A 2 nd R = A A A
41 40 pm4.71d R RingOps A B X = A X = A 2 nd R = A A A
42 relrngo Rel RingOps
43 df-rel Rel RingOps RingOps V × V
44 42 43 mpbi RingOps V × V
45 44 sseli R RingOps R V × V
46 45 adantr R RingOps A B R V × V
47 eqop R V × V R = A A A A A A 1 st R = A A A 2 nd R = A A A
48 46 47 syl R RingOps A B R = A A A A A A 1 st R = A A A 2 nd R = A A A
49 30 41 48 3bitr4d R RingOps A B X = A R = A A A A A A