Metamath Proof Explorer

Theorem dfgrp2e

Description: Alternate definition of a group as a set with a closed, associative operation, a left identity and a left inverse for each element. Alternate definition in Lang p. 7. (Contributed by NM, 10-Oct-2006) (Revised by AV, 28-Aug-2021)

		Ref	Expression
	Hypotheses	dfgrp2.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
		dfgrp2.p	⊢ + = ( +_g ‘ 𝐺 )
	Assertion	dfgrp2e	⊢ ( 𝐺 ∈ Grp ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ∧ ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfgrp2.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		dfgrp2.p	⊢ + = ( +_g ‘ 𝐺 )
3	1 2	dfgrp2	⊢ ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Smgrp ∧ ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) )
4		ax-1	⊢ ( 𝐺 ∈ V → ( 𝑛 ∈ 𝐵 → 𝐺 ∈ V ) )
5		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
6	1	eleq2i	⊢ ( 𝑛 ∈ 𝐵 ↔ 𝑛 ∈ ( Base ‘ 𝐺 ) )
7		eleq2	⊢ ( ( Base ‘ 𝐺 ) = ∅ → ( 𝑛 ∈ ( Base ‘ 𝐺 ) ↔ 𝑛 ∈ ∅ ) )
8		noel	⊢ ¬ 𝑛 ∈ ∅
9	8	pm2.21i	⊢ ( 𝑛 ∈ ∅ → 𝐺 ∈ V )
10	7 9	biimtrdi	⊢ ( ( Base ‘ 𝐺 ) = ∅ → ( 𝑛 ∈ ( Base ‘ 𝐺 ) → 𝐺 ∈ V ) )
11	6 10	biimtrid	⊢ ( ( Base ‘ 𝐺 ) = ∅ → ( 𝑛 ∈ 𝐵 → 𝐺 ∈ V ) )
12	5 11	syl	⊢ ( ¬ 𝐺 ∈ V → ( 𝑛 ∈ 𝐵 → 𝐺 ∈ V ) )
13	4 12	pm2.61i	⊢ ( 𝑛 ∈ 𝐵 → 𝐺 ∈ V )
14	13	a1d	⊢ ( 𝑛 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) → 𝐺 ∈ V ) )
15	14	rexlimiv	⊢ ( ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) → 𝐺 ∈ V )
16	1 2	issgrpv	⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ Smgrp ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ) )
17	15 16	syl	⊢ ( ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) → ( 𝐺 ∈ Smgrp ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ) )
18	17	pm5.32ri	⊢ ( ( 𝐺 ∈ Smgrp ∧ ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ∧ ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) )
19	3 18	bitri	⊢ ( 𝐺 ∈ Grp ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ∧ ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) )