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

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 ↔ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ∧ ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) )