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 = ( 1st ` R )
on1el3.2 
|- X = ran G
Assertion rngosn3 
|- ( ( R e. RingOps /\ A e. B ) -> ( X = { A } <-> R = <. { <. <. A , A >. , A >. } , { <. <. A , A >. , A >. } >. ) )

Proof

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