Metamath Proof Explorer

Theorem dfgrp3e

Description: Alternate definition of a group as a set with a closed, associative operation, for which solutions x and y of the equations ( a .+ x ) = b and ( x .+ a ) = b exist. Exercise 1 of Herstein p. 57. (Contributed by NM, 5-Dec-2006) (Revised by AV, 28-Aug-2021)

Ref Expression
Hypotheses dfgrp3.b 
|- B = ( Base ` G )
dfgrp3.p 
|- .+ = ( +g ` G )
Assertion dfgrp3e 
|- ( G e. Grp <-> ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) )

Proof

Step Hyp Ref Expression
1 dfgrp3.b 
 |-  B = ( Base ` G )
2 dfgrp3.p 
 |-  .+ = ( +g ` G )
3 1 2 dfgrp3 
 |-  ( G e. Grp <-> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) )
4 simp2 
 |-  ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> B =/= (/) )
5 sgrpmgm 
 |-  ( G e. Smgrp -> G e. Mgm )
6 5 adantr 
 |-  ( ( G e. Smgrp /\ x e. B ) -> G e. Mgm )
7 6 adantr 
 |-  ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> G e. Mgm )
8 simpr 
 |-  ( ( G e. Smgrp /\ x e. B ) -> x e. B )
9 8 adantr 
 |-  ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> x e. B )
10 simpr 
 |-  ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> y e. B )
11 1 2 mgmcl 
 |-  ( ( G e. Mgm /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
12 7 9 10 11 syl3anc 
 |-  ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> ( x .+ y ) e. B )
13 12 adantr 
 |-  ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( x .+ y ) e. B )
14 1 2 sgrpass 
 |-  ( ( G e. Smgrp /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
15 14 3anassrs 
 |-  ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ z e. B ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
16 15 ralrimiva 
 |-  ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
17 16 adantr 
 |-  ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
18 simpr 
 |-  ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) )
19 13 17 18 3jca 
 |-  ( ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) )
20 19 ex 
 |-  ( ( ( G e. Smgrp /\ x e. B ) /\ y e. B ) -> ( ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) )
21 20 ralimdva 
 |-  ( ( G e. Smgrp /\ x e. B ) -> ( A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) )
22 21 ralimdva 
 |-  ( G e. Smgrp -> ( A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) )
23 22 a1d 
 |-  ( G e. Smgrp -> ( B =/= (/) -> ( A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) -> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) ) )
24 23 3imp 
 |-  ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) )
25 4 24 jca 
 |-  ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) )
26 n0 
 |-  ( B =/= (/) <-> E. a a e. B )
27 3simpa 
 |-  ( ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) )
28 27 2ralimi 
 |-  ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) )
29 1 2 issgrpn0 
 |-  ( a e. B -> ( G e. Smgrp <-> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) ) )
30 28 29 syl5ibr 
 |-  ( a e. B -> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp ) )
31 30 exlimiv 
 |-  ( E. a a e. B -> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp ) )
32 26 31 sylbi 
 |-  ( B =/= (/) -> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp ) )
33 32 imp 
 |-  ( ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) -> G e. Smgrp )
34 simpl 
 |-  ( ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) -> B =/= (/) )
35 simp3 
 |-  ( ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) )
36 35 2ralimi 
 |-  ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) )
37 36 adantl 
 |-  ( ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) -> A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) )
38 33 34 37 3jca 
 |-  ( ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) -> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) )
39 25 38 impbii 
 |-  ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) <-> ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) )
40 3 39 bitri 
 |-  ( G e. Grp <-> ( B =/= (/) /\ A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) /\ ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) )