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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
isgrp.p ⊢ + = ( +g ‘ 𝐺 )
isgrp.z ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion isgrp ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑎 ∈ 𝐵 ∃ 𝑚 ∈ 𝐵 ( 𝑚 + 𝑎 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 isgrp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 isgrp.p ⊢ + = ( +g ‘ 𝐺 )
3 isgrp.z ⊢ 0 = ( 0g ‘ 𝐺 )
4 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
5 4 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝐵 )
6 fveq2 ⊢ ( 𝑔 = 𝐺 → ( +g ‘ 𝑔 ) = ( +g ‘ 𝐺 ) )
7 6 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( +g ‘ 𝑔 ) = + )
8 7 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑚 ( +g ‘ 𝑔 ) 𝑎 ) = ( 𝑚 + 𝑎 ) )
9 fveq2 ⊢ ( 𝑔 = 𝐺 → ( 0g ‘ 𝑔 ) = ( 0g ‘ 𝐺 ) )
10 9 3 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( 0g ‘ 𝑔 ) = 0 )
11 8 10 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑚 ( +g ‘ 𝑔 ) 𝑎 ) = ( 0g ‘ 𝑔 ) ↔ ( 𝑚 + 𝑎 ) = 0 ) )
12 5 11 rexeqbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑚 ∈ ( Base ‘ 𝑔 ) ( 𝑚 ( +g ‘ 𝑔 ) 𝑎 ) = ( 0g ‘ 𝑔 ) ↔ ∃ 𝑚 ∈ 𝐵 ( 𝑚 + 𝑎 ) = 0 ) )
13 5 12 raleqbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∃ 𝑚 ∈ ( Base ‘ 𝑔 ) ( 𝑚 ( +g ‘ 𝑔 ) 𝑎 ) = ( 0g ‘ 𝑔 ) ↔ ∀ 𝑎 ∈ 𝐵 ∃ 𝑚 ∈ 𝐵 ( 𝑚 + 𝑎 ) = 0 ) )
14 df-grp ⊢ Grp = { 𝑔 ∈ Mnd ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∃ 𝑚 ∈ ( Base ‘ 𝑔 ) ( 𝑚 ( +g ‘ 𝑔 ) 𝑎 ) = ( 0g ‘ 𝑔 ) }
15 13 14 elrab2 ⊢ ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑎 ∈ 𝐵 ∃ 𝑚 ∈ 𝐵 ( 𝑚 + 𝑎 ) = 0 ) )