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 No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion issgrp Could not format assertion : No typesetting found for |- ( 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 ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 issgrp.b B = Base M
2 issgrp.o Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |-
3 fvexd g = M Base g 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 V
7 fveq2 g = M + g = + M
8 7 adantr g = M b = B + g = + M
9 8 2 eqtr4di Could not format ( ( g = M /\ b = B ) -> ( +g ` g ) = .o. ) : No typesetting found for |- ( ( g = M /\ b = B ) -> ( +g ` g ) = .o. ) with typecode |-
10 simplr Could not format ( ( ( g = M /\ b = B ) /\ o = .o. ) -> b = B ) : No typesetting found for |- ( ( ( g = M /\ b = B ) /\ o = .o. ) -> b = B ) with typecode |-
11 id Could not format ( o = .o. -> o = .o. ) : No typesetting found for |- ( o = .o. -> o = .o. ) with typecode |-
12 oveq Could not format ( o = .o. -> ( x o y ) = ( x .o. y ) ) : No typesetting found for |- ( o = .o. -> ( x o y ) = ( x .o. y ) ) with typecode |-
13 eqidd Could not format ( o = .o. -> z = z ) : No typesetting found for |- ( o = .o. -> z = z ) with typecode |-
14 11 12 13 oveq123d Could not format ( o = .o. -> ( ( x o y ) o z ) = ( ( x .o. y ) .o. z ) ) : No typesetting found for |- ( o = .o. -> ( ( x o y ) o z ) = ( ( x .o. y ) .o. z ) ) with typecode |-
15 eqidd Could not format ( o = .o. -> x = x ) : No typesetting found for |- ( o = .o. -> x = x ) with typecode |-
16 oveq Could not format ( o = .o. -> ( y o z ) = ( y .o. z ) ) : No typesetting found for |- ( o = .o. -> ( y o z ) = ( y .o. z ) ) with typecode |-
17 11 15 16 oveq123d Could not format ( o = .o. -> ( x o ( y o z ) ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( o = .o. -> ( x o ( y o z ) ) = ( x .o. ( y .o. z ) ) ) with typecode |-
18 14 17 eqeq12d Could not format ( o = .o. -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( o = .o. -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
19 18 adantl Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
20 10 19 raleqbidv Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
21 10 20 raleqbidv Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
22 10 21 raleqbidv Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
23 6 9 22 sbcied2 Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
24 3 5 23 sbcied2 Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
25 df-sgrp Could not format 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 ) ) } : No typesetting found for |- 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 ) ) } with typecode |-
26 24 25 elrab2 Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-