Metamath Proof Explorer

Theorem issgrp

Description: The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020)

Ref Expression
Hypotheses issgrp.b 
|- B = ( Base ` M )
issgrp.o 
|- .o. = ( +g ` M )
Assertion issgrp 
|- ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )

Proof

Step Hyp Ref Expression
1 issgrp.b 
 |-  B = ( Base ` M )
2 issgrp.o 
 |-  .o. = ( +g ` M )
3 fvexd 
 |-  ( g = M -> ( Base ` g ) e. _V )
4 fveq2 
 |-  ( g = M -> ( Base ` g ) = ( Base ` M ) )
5 4 1 eqtr4di 
 |-  ( g = M -> ( Base ` g ) = B )
6 fvexd 
 |-  ( ( g = M /\ b = B ) -> ( +g ` g ) e. _V )
7 fveq2 
 |-  ( g = M -> ( +g ` g ) = ( +g ` M ) )
8 7 adantr 
 |-  ( ( g = M /\ b = B ) -> ( +g ` g ) = ( +g ` M ) )
9 8 2 eqtr4di 
 |-  ( ( g = M /\ b = B ) -> ( +g ` g ) = .o. )
10 simplr 
 |-  ( ( ( g = M /\ b = B ) /\ o = .o. ) -> b = B )
11 id 
 |-  ( o = .o. -> o = .o. )
12 oveq 
 |-  ( o = .o. -> ( x o y ) = ( x .o. y ) )
13 eqidd 
 |-  ( o = .o. -> z = z )
14 11 12 13 oveq123d 
 |-  ( o = .o. -> ( ( x o y ) o z ) = ( ( x .o. y ) .o. z ) )
15 eqidd 
 |-  ( o = .o. -> x = x )
16 oveq 
 |-  ( o = .o. -> ( y o z ) = ( y .o. z ) )
17 11 15 16 oveq123d 
 |-  ( o = .o. -> ( x o ( y o z ) ) = ( x .o. ( y .o. z ) ) )
18 14 17 eqeq12d 
 |-  ( o = .o. -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
19 18 adantl 
 |-  ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
20 10 19 raleqbidv 
 |-  ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
21 10 20 raleqbidv 
 |-  ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
22 10 21 raleqbidv 
 |-  ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
23 6 9 22 sbcied2 
 |-  ( ( g = M /\ b = B ) -> ( [. ( +g ` g ) / o ]. A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
24 3 5 23 sbcied2 
 |-  ( g = M -> ( [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
25 df-sgrp 
 |-  Smgrp = { g e. Mgm | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) }
26 24 25 elrab2 
 |-  ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )