Theorem isgrpi

Description: Properties that determine a group. N (negative) is normally dependent on x i.e. read it as N ( x ) . (Contributed by NM, 3-Sep-2011)

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

Proof

Step	Hyp	Ref	Expression
1		isgrpi.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		isgrpi.p	⊢ + = ( +g ‘ 𝐺 )
3		isgrpi.c	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
4		isgrpi.a	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
5		isgrpi.z	⊢ 0 ∈ 𝐵
6		isgrpi.i	⊢ ( 𝑥 ∈ 𝐵 → ( 0 + 𝑥 ) = 𝑥 )
7		isgrpi.n	⊢ ( 𝑥 ∈ 𝐵 → 𝑁 ∈ 𝐵 )
8		isgrpi.j	⊢ ( 𝑥 ∈ 𝐵 → ( 𝑁 + 𝑥 ) = 0 )
9	1	a1i	⊢ ( ⊤ → 𝐵 = ( Base ‘ 𝐺 ) )
10	2	a1i	⊢ ( ⊤ → + = ( +g ‘ 𝐺 ) )
11	3	3adant1	⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
12	4	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
13	5	a1i	⊢ ( ⊤ → 0 ∈ 𝐵 )
14	6	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
15	7	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ 𝐵 )
16	8	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → ( 𝑁 + 𝑥 ) = 0 )
17	9 10 11 12 13 14 15 16	isgrpd	⊢ ( ⊤ → 𝐺 ∈ Grp )
18	17	mptru	⊢ 𝐺 ∈ Grp