Description: If there is a left and right identity element for any binary operation (group operation) .+ , both identity elements are equal. Generalization of statement in Lang p. 3: it is sufficient that "e" is a left identity element and "e``" is a right identity element instead of both being (two-sided) identity elements. (Contributed by AV, 26-Dec-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | lidrideqd.l | ⊢ ( 𝜑 → 𝐿 ∈ 𝐵 ) | |
| lidrideqd.r | ⊢ ( 𝜑 → 𝑅 ∈ 𝐵 ) | ||
| lidrideqd.li | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝐿 + 𝑥 ) = 𝑥 ) | ||
| lidrideqd.ri | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑅 ) = 𝑥 ) | ||
| Assertion | lidrideqd | ⊢ ( 𝜑 → 𝐿 = 𝑅 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lidrideqd.l | ⊢ ( 𝜑 → 𝐿 ∈ 𝐵 ) | |
| 2 | lidrideqd.r | ⊢ ( 𝜑 → 𝑅 ∈ 𝐵 ) | |
| 3 | lidrideqd.li | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝐿 + 𝑥 ) = 𝑥 ) | |
| 4 | lidrideqd.ri | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑅 ) = 𝑥 ) | |
| 5 | oveq1 | ⊢ ( 𝑥 = 𝐿 → ( 𝑥 + 𝑅 ) = ( 𝐿 + 𝑅 ) ) | |
| 6 | id | ⊢ ( 𝑥 = 𝐿 → 𝑥 = 𝐿 ) | |
| 7 | 5 6 | eqeq12d | ⊢ ( 𝑥 = 𝐿 → ( ( 𝑥 + 𝑅 ) = 𝑥 ↔ ( 𝐿 + 𝑅 ) = 𝐿 ) ) |
| 8 | 7 4 1 | rspcdva | ⊢ ( 𝜑 → ( 𝐿 + 𝑅 ) = 𝐿 ) |
| 9 | oveq2 | ⊢ ( 𝑥 = 𝑅 → ( 𝐿 + 𝑥 ) = ( 𝐿 + 𝑅 ) ) | |
| 10 | id | ⊢ ( 𝑥 = 𝑅 → 𝑥 = 𝑅 ) | |
| 11 | 9 10 | eqeq12d | ⊢ ( 𝑥 = 𝑅 → ( ( 𝐿 + 𝑥 ) = 𝑥 ↔ ( 𝐿 + 𝑅 ) = 𝑅 ) ) |
| 12 | 11 3 2 | rspcdva | ⊢ ( 𝜑 → ( 𝐿 + 𝑅 ) = 𝑅 ) |
| 13 | 8 12 | eqtr3d | ⊢ ( 𝜑 → 𝐿 = 𝑅 ) |