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	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
	isgrpd2.p	⊢ ( 𝜑 → + = ( +_g ‘ 𝐺 ) )
	isgrpd2.z	⊢ ( 𝜑 → 0 = ( 0_g ‘ 𝐺 ) )
	isgrpd2.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
	isgrpd2.n	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ 𝐵 )
	isgrpd2.j	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑁 + 𝑥 ) = 0 )
Assertion	isgrpd2	⊢ ( 𝜑 → 𝐺 ∈ Grp )

Proof

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

Metamath Proof Explorer

Theorem isgrpd2

Proof