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 ) )