| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ringidcl | Structured version Visualization version GIF version | ||
| Description: The unity element of a ring belongs to the base set of the ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| Ref | Expression |
|---|---|
| ringidcl.b | ⊢ 𝐵 = (Base‘𝑅) |
| ringidcl.u | ⊢ 1 = (1r‘𝑅) |
| Ref | Expression |
|---|---|
| ringidcl | ⊢ (𝑅 ∈ Ring → 1 ∈ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2737 | . . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅) | |
| 2 | 1 | ringmgp 20236 | . 2 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd) |
| 3 | ringidcl.b | . . . 4 ⊢ 𝐵 = (Base‘𝑅) | |
| 4 | 1, 3 | mgpbas 20142 | . . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅)) |
| 5 | ringidcl.u | . . . 4 ⊢ 1 = (1r‘𝑅) | |
| 6 | 1, 5 | ringidval 20180 | . . 3 ⊢ 1 = (0g‘(mulGrp‘𝑅)) |
| 7 | 4, 6 | mndidcl 18762 | . 2 ⊢ ((mulGrp‘𝑅) ∈ Mnd → 1 ∈ 𝐵) |
| 8 | 2, 7 | syl 17 | 1 ⊢ (𝑅 ∈ Ring → 1 ∈ 𝐵) |
| Copyright terms: Public domain | W3C validator |