Theorem isgrpd2 19018

Description: Deduce a group from its properties. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). Note: normally we don't use a 𝜑 antecedent on hypotheses that name structure components, since they can be eliminated with eqid 2763, but we make an exception for theorems such as isgrpd2 19018, ismndd 18809, and islmodd 20987 since theorems using them often rewrite the structure components. (Contributed by NM, 10-Aug-2013.)

Hypotheses

Ref	Expression
isgrpd2.b	⊢ (𝜑 → 𝐵 = (Base‘𝐺))
isgrpd2.p	⊢ (𝜑 → + = (+g‘𝐺))
isgrpd2.z	⊢ (𝜑 → 0 = (0g‘𝐺))
isgrpd2.g	⊢ (𝜑 → 𝐺 ∈ Mnd)
isgrpd2.n	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵)
isgrpd2.j	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 )

Assertion

Ref	Expression
isgrpd2	⊢ (𝜑 → 𝐺 ∈ Grp)

Distinct variable groups:   𝑥, +   𝑥,𝐵   𝑥,𝐺   𝜑,𝑥

Allowed substitution hints:   𝑁(𝑥)   0 (𝑥)

Proof of Theorem isgrpd2

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isgrpd2.b	. 2 ⊢ (𝜑 → 𝐵 = (Base‘𝐺))
2		isgrpd2.p	. 2 ⊢ (𝜑 → + = (+g‘𝐺))
3		isgrpd2.z	. 2 ⊢ (𝜑 → 0 = (0g‘𝐺))
4		isgrpd2.g	. 2 ⊢ (𝜑 → 𝐺 ∈ Mnd)
5		isgrpd2.n	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵)
6		isgrpd2.j	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 )
7		oveq1 7417	. . . . 5 ⊢ (𝑦 = 𝑁 → (𝑦 + 𝑥) = (𝑁 + 𝑥))
8	7	eqeq1d 2765	. . . 4 ⊢ (𝑦 = 𝑁 → ((𝑦 + 𝑥) = 0 ↔ (𝑁 + 𝑥) = 0 ))
9	8	rspcev 3581	. . 3 ⊢ ((𝑁 ∈ 𝐵 ∧ (𝑁 + 𝑥) = 0 ) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )
10	5, 6, 9	syl2anc 595	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )
11	1, 2, 3, 4, 10	isgrpd2e 19017	1 ⊢ (𝜑 → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∃wrex 3089  ‘cfv 6536  (class class class)co 7410  Basecbs 17264  +_gcplusg 17305  0_gc0g 17487  Mndcmnd 18787  Grpcgrp 18995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-grp 18998

This theorem is referenced by:  prdsgrpd  19111  oppggrp  19422