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 𝐺 = ( 1st𝑅 )
on1el3.2 𝑋 = ran 𝐺
Assertion rngosn3 ( ( 𝑅 ∈ RingOps ∧ 𝐴𝐵 ) → ( 𝑋 = { 𝐴 } ↔ 𝑅 = ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ) )

Proof

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