Description: The only (unital) ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption R e. Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 14-Feb-2010) (Revised by AV, 25-Jan-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ring1zr.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
| ring1zr.p | ⊢ + = ( +g ‘ 𝑅 ) | ||
| ring1zr.t | ⊢ ∗ = ( .r ‘ 𝑅 ) | ||
| Assertion | rngen1zr | ⊢ ( ( ( 𝑅 ∈ Ring ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 ≈ 1o ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ring1zr.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
| 2 | ring1zr.p | ⊢ + = ( +g ‘ 𝑅 ) | |
| 3 | ring1zr.t | ⊢ ∗ = ( .r ‘ 𝑅 ) | |
| 4 | en1eqsnbi | ⊢ ( 𝑍 ∈ 𝐵 → ( 𝐵 ≈ 1o ↔ 𝐵 = { 𝑍 } ) ) | |
| 5 | 4 | adantl | ⊢ ( ( ( 𝑅 ∈ Ring ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 ≈ 1o ↔ 𝐵 = { 𝑍 } ) ) |
| 6 | 1 2 3 | ring1zr | ⊢ ( ( ( 𝑅 ∈ Ring ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) ) |
| 7 | 5 6 | bitrd | ⊢ ( ( ( 𝑅 ∈ Ring ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 ≈ 1o ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) ) |