This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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