Description: The multiplicative identity is the unique element of the ring that is left- and right-neutral on all elements under multiplication. (Contributed by Mario Carneiro, 10-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dfur2.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
| dfur2.t | ⊢ · = ( .r ‘ 𝑅 ) | ||
| dfur2.u | ⊢ 1 = ( 1r ‘ 𝑅 ) | ||
| Assertion | dfur2 | ⊢ 1 = ( ℩ 𝑒 ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfur2.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
| 2 | dfur2.t | ⊢ · = ( .r ‘ 𝑅 ) | |
| 3 | dfur2.u | ⊢ 1 = ( 1r ‘ 𝑅 ) | |
| 4 | eqid | ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 ) | |
| 5 | 4 1 | mgpbas | ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) |
| 6 | 4 2 | mgpplusg | ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) ) |
| 7 | 4 3 | ringidval | ⊢ 1 = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) |
| 8 | 5 6 7 | grpidval | ⊢ 1 = ( ℩ 𝑒 ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 𝑒 ) = 𝑥 ) ) ) |