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	|- ( ph -> B = ( Base ` G ) )
	isgrpd2.p	|- ( ph -> .+ = ( +g ` G ) )
	isgrpd2.z	|- ( ph -> .0. = ( 0g ` G ) )
	isgrpd2.g	|- ( ph -> G e. Mnd )
	isgrpd2.n	|- ( ( ph /\ x e. B ) -> N e. B )
	isgrpd2.j	|- ( ( ph /\ x e. B ) -> ( N .+ x ) = .0. )
Assertion	isgrpd2	|- ( ph -> G e. Grp )

Proof

Step	Hyp	Ref	Expression
1		isgrpd2.b	|- ( ph -> B = ( Base ` G ) )
2		isgrpd2.p	|- ( ph -> .+ = ( +g ` G ) )
3		isgrpd2.z	|- ( ph -> .0. = ( 0g ` G ) )
4		isgrpd2.g	|- ( ph -> G e. Mnd )
5		isgrpd2.n	|- ( ( ph /\ x e. B ) -> N e. B )
6		isgrpd2.j	|- ( ( ph /\ x e. B ) -> ( N .+ x ) = .0. )
7		oveq1	|- ( y = N -> ( y .+ x ) = ( N .+ x ) )
8	7	eqeq1d	|- ( y = N -> ( ( y .+ x ) = .0. <-> ( N .+ x ) = .0. ) )
9	8	rspcev	|- ( ( N e. B /\ ( N .+ x ) = .0. ) -> E. y e. B ( y .+ x ) = .0. )
10	5 6 9	syl2anc	|- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = .0. )
11	1 2 3 4 10	isgrpd2e	|- ( ph -> G e. Grp )