isgrpd2

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

	Ref	Expression
Hypotheses	isgrpd2.b	$⊢ φ \to B = {Base}_{G}$
	isgrpd2.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
	isgrpd2.z	$⊢ φ \to \underset{˙}{0} = 0_{G}$
	isgrpd2.g	$⊢ φ \to G \in Mnd$
	isgrpd2.n	$⊢ (φ \land x \in B) \to N \in B$
	isgrpd2.j	$⊢ (φ \land x \in B) \to N \underset{˙}{+} x = \underset{˙}{0}$
Assertion	isgrpd2	$⊢ φ \to G \in Grp$

Proof

Step	Hyp	Ref	Expression
1		isgrpd2.b	$⊢ φ \to B = {Base}_{G}$
2		isgrpd2.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
3		isgrpd2.z	$⊢ φ \to \underset{˙}{0} = 0_{G}$
4		isgrpd2.g	$⊢ φ \to G \in Mnd$
5		isgrpd2.n	$⊢ (φ \land x \in B) \to N \in B$
6		isgrpd2.j	$⊢ (φ \land x \in B) \to N \underset{˙}{+} x = \underset{˙}{0}$
7		oveq1	$⊢ y = N \to y \underset{˙}{+} x = N \underset{˙}{+} x$
8	7	eqeq1d	$⊢ y = N \to (y \underset{˙}{+} x = \underset{˙}{0} \leftrightarrow N \underset{˙}{+} x = \underset{˙}{0})$
9	8	rspcev	$⊢ (N \in B \land N \underset{˙}{+} x = \underset{˙}{0}) \to \exists y \in B y \underset{˙}{+} x = \underset{˙}{0}$
10	5 6 9	syl2anc	$⊢ (φ \land x \in B) \to \exists y \in B y \underset{˙}{+} x = \underset{˙}{0}$
11	1 2 3 4 10	isgrpd2e	$⊢ φ \to G \in Grp$

Metamath Proof Explorer

Theorem isgrpd2

Proof