Database
BASIC ALGEBRAIC STRUCTURES
Groups
Definition and basic properties
isgrpix
Metamath Proof Explorer
Description: Properties that determine a group. Read N as N ( x ) . Note:
This theorem has hard-coded structure indices for demonstration
purposes. It is not intended for general use.
(New usage is discouraged.) (Contributed by NM , 4-Sep-2011)
Ref
Expression
Hypotheses
isgrpix.a
⊢ B ∈ V
isgrpix.b
⊢ + ˙ ∈ V
isgrpix.g
⊢ G = 1 B 2 + ˙
isgrpix.2
⊢ x ∈ B ∧ y ∈ B → x + ˙ y ∈ B
isgrpix.3
⊢ x ∈ B ∧ y ∈ B ∧ z ∈ B → x + ˙ y + ˙ z = x + ˙ y + ˙ z
isgrpix.z
⊢ 0 ˙ ∈ B
isgrpix.5
⊢ x ∈ B → 0 ˙ + ˙ x = x
isgrpix.6
⊢ x ∈ B → N ∈ B
isgrpix.7
⊢ x ∈ B → N + ˙ x = 0 ˙
Assertion
isgrpix
⊢ G ∈ Grp
Proof
Step
Hyp
Ref
Expression
1
isgrpix.a
⊢ B ∈ V
2
isgrpix.b
⊢ + ˙ ∈ V
3
isgrpix.g
⊢ G = 1 B 2 + ˙
4
isgrpix.2
⊢ x ∈ B ∧ y ∈ B → x + ˙ y ∈ B
5
isgrpix.3
⊢ x ∈ B ∧ y ∈ B ∧ z ∈ B → x + ˙ y + ˙ z = x + ˙ y + ˙ z
6
isgrpix.z
⊢ 0 ˙ ∈ B
7
isgrpix.5
⊢ x ∈ B → 0 ˙ + ˙ x = x
8
isgrpix.6
⊢ x ∈ B → N ∈ B
9
isgrpix.7
⊢ x ∈ B → N + ˙ x = 0 ˙
10
1 2 3
grpbasex
⊢ B = Base G
11
1 2 3
grpplusgx
⊢ + ˙ = + G
12
10 11 4 5 6 7 8 9
isgrpi
⊢ G ∈ Grp