Theorem isgrpd2e

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

	Ref	Expression
Hypotheses	isgrpd2.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
	isgrpd2.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
	isgrpd2.z	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐺 ) )
	isgrpd2.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
	isgrpd2e.n	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 )
Assertion	isgrpd2e	⊢ ( 𝜑 → 𝐺 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		isgrpd2.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
2		isgrpd2.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
3		isgrpd2.z	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝐺 ) )
4		isgrpd2.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
5		isgrpd2e.n	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 )
6	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 )
7	2	oveqd	⊢ ( 𝜑 → ( 𝑦 + 𝑥 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
8	7 3	eqeq12d	⊢ ( 𝜑 → ( ( 𝑦 + 𝑥 ) = 0 ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
9	1 8	rexeqbidv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 ↔ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
10	1 9	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( 𝑦 + 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
11	6 10	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
12		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
13		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
14		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
15	12 13 14	isgrp	⊢ ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
16	4 11 15	sylanbrc	⊢ ( 𝜑 → 𝐺 ∈ Grp )