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 imbitrdi ⊢ ( ( 𝑅 ∈ 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 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑋 = { 𝐴 } ↔ 𝑅 = ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ) )