Theorem 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	$$⊢\phi \to B={\mathrm{Base}}_G$$
	isgrpd2.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
	isgrpd2.z	$$⊢\phi \to \underset{\dot{}}{0}=0_G$$
	isgrpd2.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	isgrpd2.n	$$⊢\left(\phi \wedge x\in B\right)\to N\in B$$
	isgrpd2.j	$$⊢\left(\phi \wedge x\in B\right)\to N\underset{\dot{}}{+}x=\underset{\dot{}}{0}$$
Assertion	isgrpd2	$$⊢\phi \to G\in \mathrm{Grp}$$

Proof

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