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}\left({R}\right)$
on1el3.2 ${⊢}{X}=\mathrm{ran}{G}$
Assertion rngosn3 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {B}\right)\to \left({X}=\left\{{A}\right\}↔{R}=⟨\left\{⟨⟨{A},{A}⟩,{A}⟩\right\},\left\{⟨⟨{A},{A}⟩,{A}⟩\right\}⟩\right)$

Proof

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