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

Metamath Proof Explorer

Theorem dfgrp2

Description: Alternate definition of a group as semigroup with a left identity and a left inverse for each element. This "definition" is weaker than df-grp , based on the definition of a monoid which provides a left and a right identity. (Contributed by AV, 28-Aug-2021)

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

Proof

Step Hyp Ref Expression
1 dfgrp2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 dfgrp2.p ⊢ + = ( +g ‘ 𝐺 )
3 grpsgrp ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Smgrp )
4 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
5 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6 1 5 mndidcl ⊢ ( 𝐺 ∈ Mnd → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
7 4 6 syl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
8 oveq1 ⊢ ( 𝑛 = ( 0g ‘ 𝐺 ) → ( 𝑛 + 𝑥 ) = ( ( 0g ‘ 𝐺 ) + 𝑥 ) )
9 8 eqeq1d ⊢ ( 𝑛 = ( 0g ‘ 𝐺 ) → ( ( 𝑛 + 𝑥 ) = 𝑥 ↔ ( ( 0g ‘ 𝐺 ) + 𝑥 ) = 𝑥 ) )
10 eqeq2 ⊢ ( 𝑛 = ( 0g ‘ 𝐺 ) → ( ( 𝑖 + 𝑥 ) = 𝑛 ↔ ( 𝑖 + 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
11 10 rexbidv ⊢ ( 𝑛 = ( 0g ‘ 𝐺 ) → ( ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ↔ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
12 9 11 anbi12d ⊢ ( 𝑛 = ( 0g ‘ 𝐺 ) → ( ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ↔ ( ( ( 0g ‘ 𝐺 ) + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = ( 0g ‘ 𝐺 ) ) ) )
13 12 ralbidv ⊢ ( 𝑛 = ( 0g ‘ 𝐺 ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( ( 0g ‘ 𝐺 ) + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = ( 0g ‘ 𝐺 ) ) ) )
14 13 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑛 = ( 0g ‘ 𝐺 ) ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( ( 0g ‘ 𝐺 ) + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = ( 0g ‘ 𝐺 ) ) ) )
15 1 2 5 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑥 ) = 𝑥 )
16 4 15 sylan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑥 ) = 𝑥 )
17 1 2 5 grpinvex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = ( 0g ‘ 𝐺 ) )
18 16 17 jca ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 0g ‘ 𝐺 ) + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
19 18 ralrimiva ⊢ ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ 𝐵 ( ( ( 0g ‘ 𝐺 ) + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
20 7 14 19 rspcedvd ⊢ ( 𝐺 ∈ Grp → ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) )
21 3 20 jca ⊢ ( 𝐺 ∈ Grp → ( 𝐺 ∈ Smgrp ∧ ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) )
22 1 a1i ⊢ ( ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ∧ 𝐺 ∈ Smgrp ) → 𝐵 = ( Base ‘ 𝐺 ) )
23 2 a1i ⊢ ( ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ∧ 𝐺 ∈ Smgrp ) → + = ( +g ‘ 𝐺 ) )
24 sgrpmgm ⊢ ( 𝐺 ∈ Smgrp → 𝐺 ∈ Mgm )
25 24 adantl ⊢ ( ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ∧ 𝐺 ∈ Smgrp ) → 𝐺 ∈ Mgm )
26 1 2 mgmcl ⊢ ( ( 𝐺 ∈ Mgm ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 + 𝑏 ) ∈ 𝐵 )
27 25 26 syl3an1 ⊢ ( ( ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ∧ 𝐺 ∈ Smgrp ) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 + 𝑏 ) ∈ 𝐵 )
28 1 2 sgrpass ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 + 𝑏 ) + 𝑐 ) = ( 𝑎 + ( 𝑏 + 𝑐 ) ) )
29 28 adantll ⊢ ( ( ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ∧ 𝐺 ∈ Smgrp ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 + 𝑏 ) + 𝑐 ) = ( 𝑎 + ( 𝑏 + 𝑐 ) ) )
30 simpll ⊢ ( ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ∧ 𝐺 ∈ Smgrp ) → 𝑛 ∈ 𝐵 )
31 oveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑛 + 𝑥 ) = ( 𝑛 + 𝑎 ) )
32 id ⊢ ( 𝑥 = 𝑎 → 𝑥 = 𝑎 )
33 31 32 eqeq12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑛 + 𝑥 ) = 𝑥 ↔ ( 𝑛 + 𝑎 ) = 𝑎 ) )
34 oveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑖 + 𝑥 ) = ( 𝑖 + 𝑎 ) )
35 34 eqeq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑖 + 𝑥 ) = 𝑛 ↔ ( 𝑖 + 𝑎 ) = 𝑛 ) )
36 35 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ↔ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑛 ) )
37 33 36 anbi12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ↔ ( ( 𝑛 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑛 ) ) )
38 37 rspcv ⊢ ( 𝑎 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) → ( ( 𝑛 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑛 ) ) )
39 simpl ⊢ ( ( ( 𝑛 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑛 ) → ( 𝑛 + 𝑎 ) = 𝑎 )
40 38 39 syl6com ⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) → ( 𝑎 ∈ 𝐵 → ( 𝑛 + 𝑎 ) = 𝑎 ) )
41 40 ad2antlr ⊢ ( ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ∧ 𝐺 ∈ Smgrp ) → ( 𝑎 ∈ 𝐵 → ( 𝑛 + 𝑎 ) = 𝑎 ) )
42 41 imp ⊢ ( ( ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ∧ 𝐺 ∈ Smgrp ) ∧ 𝑎 ∈ 𝐵 ) → ( 𝑛 + 𝑎 ) = 𝑎 )
43 oveq1 ⊢ ( 𝑖 = 𝑏 → ( 𝑖 + 𝑎 ) = ( 𝑏 + 𝑎 ) )
44 43 eqeq1d ⊢ ( 𝑖 = 𝑏 → ( ( 𝑖 + 𝑎 ) = 𝑛 ↔ ( 𝑏 + 𝑎 ) = 𝑛 ) )
45 44 cbvrexvw ⊢ ( ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑛 ↔ ∃ 𝑏 ∈ 𝐵 ( 𝑏 + 𝑎 ) = 𝑛 )
46 45 biimpi ⊢ ( ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑛 → ∃ 𝑏 ∈ 𝐵 ( 𝑏 + 𝑎 ) = 𝑛 )
47 46 adantl ⊢ ( ( ( 𝑛 + 𝑎 ) = 𝑎 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑎 ) = 𝑛 ) → ∃ 𝑏 ∈ 𝐵 ( 𝑏 + 𝑎 ) = 𝑛 )
48 38 47 syl6com ⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) → ( 𝑎 ∈ 𝐵 → ∃ 𝑏 ∈ 𝐵 ( 𝑏 + 𝑎 ) = 𝑛 ) )
49 48 ad2antlr ⊢ ( ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ∧ 𝐺 ∈ Smgrp ) → ( 𝑎 ∈ 𝐵 → ∃ 𝑏 ∈ 𝐵 ( 𝑏 + 𝑎 ) = 𝑛 ) )
50 49 imp ⊢ ( ( ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ∧ 𝐺 ∈ Smgrp ) ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑏 ∈ 𝐵 ( 𝑏 + 𝑎 ) = 𝑛 )
51 22 23 27 29 30 42 50 isgrpde ⊢ ( ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) ∧ 𝐺 ∈ Smgrp ) → 𝐺 ∈ Grp )
52 51 ex ⊢ ( ( 𝑛 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) → ( 𝐺 ∈ Smgrp → 𝐺 ∈ Grp ) )
53 52 rexlimiva ⊢ ( ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) → ( 𝐺 ∈ Smgrp → 𝐺 ∈ Grp ) )
54 53 impcom ⊢ ( ( 𝐺 ∈ Smgrp ∧ ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) → 𝐺 ∈ Grp )
55 21 54 impbii ⊢ ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Smgrp ∧ ∃ 𝑛 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑛 + 𝑥 ) = 𝑥 ∧ ∃ 𝑖 ∈ 𝐵 ( 𝑖 + 𝑥 ) = 𝑛 ) ) )