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

Metamath Proof Explorer

Theorem isgrp

Description: The predicate "is a group". (This theorem demonstrates the use of symbols as variable names, first proposed by FL in 2010.) (Contributed by NM, 17-Oct-2012) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses isgrp.b ⊢ B = Base G
isgrp.p ⊢ + ˙ = + G
isgrp.z ⊢ 0 ˙ = 0 G
Assertion isgrp ⊢ G ∈ Grp ↔ G ∈ Mnd ∧ ∀ a ∈ B ∃ m ∈ B m + ˙ a = 0 ˙

Proof

Step Hyp Ref Expression
1 isgrp.b ⊢ B = Base G
2 isgrp.p ⊢ + ˙ = + G
3 isgrp.z ⊢ 0 ˙ = 0 G
4 fveq2 ⊢ g = G → Base g = Base G
5 4 1 eqtr4di ⊢ g = G → Base g = B
6 fveq2 ⊢ g = G → + g = + G
7 6 2 eqtr4di ⊢ g = G → + g = + ˙
8 7 oveqd ⊢ g = G → m + g a = m + ˙ a
9 fveq2 ⊢ g = G → 0 g = 0 G
10 9 3 eqtr4di ⊢ g = G → 0 g = 0 ˙
11 8 10 eqeq12d ⊢ g = G → m + g a = 0 g ↔ m + ˙ a = 0 ˙
12 5 11 rexeqbidv ⊢ g = G → ∃ m ∈ Base g m + g a = 0 g ↔ ∃ m ∈ B m + ˙ a = 0 ˙
13 5 12 raleqbidv ⊢ g = G → ∀ a ∈ Base g ∃ m ∈ Base g m + g a = 0 g ↔ ∀ a ∈ B ∃ m ∈ B m + ˙ a = 0 ˙
14 df-grp ⊢ Grp = g ∈ Mnd | ∀ a ∈ Base g ∃ m ∈ Base g m + g a = 0 g
15 13 14 elrab2 ⊢ G ∈ Grp ↔ G ∈ Mnd ∧ ∀ a ∈ B ∃ m ∈ B m + ˙ a = 0 ˙