Theorem isgrpde

Description: Deduce a group from its properties. In this version of isgrpd , we don't assume there is an expression for the inverse of x . (Contributed by NM, 6-Jan-2015)

	Ref	Expression
Hypotheses	isgrpd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
	isgrpd.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
	isgrpd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
	isgrpd.a	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
	isgrpd.z	⊢ ( 𝜑 → 0 ∈ 𝐵 )
	isgrpd.i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
	isgrpde.n	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 )
Assertion	isgrpde	⊢ ( 𝜑 → 𝐺 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		isgrpd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
2		isgrpd.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
3		isgrpd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
4		isgrpd.a	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
5		isgrpd.z	⊢ ( 𝜑 → 0 ∈ 𝐵 )
6		isgrpd.i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
7		isgrpde.n	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 )
8	3 5 6 4 7	grpridd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
9	1 2 5 6 8	grpidd	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐺 ) )
10	1 2 3 4 5 6 8	ismndd	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
11	1 2 9 10 7	isgrpd2e	⊢ ( 𝜑 → 𝐺 ∈ Grp )