Description: Deduce a group from its properties. Unlike isgrpd2 , this one goes straight from the base properties rather than going through Mnd . N (negative) is normally dependent on x i.e. read it as N ( x ) . (Contributed by NM, 6-Jun-2013) (Revised by Mario Carneiro, 6-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | isgrpd.b | ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) ) | |
| isgrpd.p | ⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) ) | ||
| isgrpd.c | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 ) | ||
| isgrpd.a | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) | ||
| isgrpd.z | ⊢ ( 𝜑 → 0 ∈ 𝐵 ) | ||
| isgrpd.i | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 ) | ||
| isgrpd.n | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ 𝐵 ) | ||
| isgrpd.j | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑁 + 𝑥 ) = 0 ) | ||
| Assertion | isgrpd | ⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isgrpd.b | ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) ) | |
| 2 | isgrpd.p | ⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) ) | |
| 3 | isgrpd.c | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 ) | |
| 4 | isgrpd.a | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) | |
| 5 | isgrpd.z | ⊢ ( 𝜑 → 0 ∈ 𝐵 ) | |
| 6 | isgrpd.i | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 ) | |
| 7 | isgrpd.n | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ 𝐵 ) | |
| 8 | isgrpd.j | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑁 + 𝑥 ) = 0 ) | |
| 9 | oveq1 | ⊢ ( 𝑦 = 𝑁 → ( 𝑦 + 𝑥 ) = ( 𝑁 + 𝑥 ) ) | |
| 10 | 9 | eqeq1d | ⊢ ( 𝑦 = 𝑁 → ( ( 𝑦 + 𝑥 ) = 0 ↔ ( 𝑁 + 𝑥 ) = 0 ) ) |
| 11 | 10 | rspcev | ⊢ ( ( 𝑁 ∈ 𝐵 ∧ ( 𝑁 + 𝑥 ) = 0 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 ) |
| 12 | 7 8 11 | syl2anc | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 ) |
| 13 | 1 2 3 4 5 6 12 | isgrpde | ⊢ ( 𝜑 → 𝐺 ∈ Grp ) |