Metamath Proof Explorer


Theorem ismnddef

Description: The predicate "is a monoid", corresponding 1-to-1 to the definition. (Contributed by FL, 2-Nov-2009) (Revised by AV, 1-Feb-2020)

Ref Expression
Hypotheses ismnddef.b B = Base G
ismnddef.p + ˙ = + G
Assertion ismnddef Could not format assertion : No typesetting found for |- ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 ismnddef.b B = Base G
2 ismnddef.p + ˙ = + G
3 fvex Base g V
4 fvex + g V
5 fveq2 g = G Base g = Base G
6 5 1 eqtr4di g = G Base g = B
7 6 eqeq2d g = G b = Base g b = B
8 fveq2 g = G + g = + G
9 8 2 eqtr4di g = G + g = + ˙
10 9 eqeq2d g = G p = + g p = + ˙
11 7 10 anbi12d g = G b = Base g p = + g b = B p = + ˙
12 simpl b = B p = + ˙ b = B
13 oveq p = + ˙ e p a = e + ˙ a
14 13 eqeq1d p = + ˙ e p a = a e + ˙ a = a
15 oveq p = + ˙ a p e = a + ˙ e
16 15 eqeq1d p = + ˙ a p e = a a + ˙ e = a
17 14 16 anbi12d p = + ˙ e p a = a a p e = a e + ˙ a = a a + ˙ e = a
18 17 adantl b = B p = + ˙ e p a = a a p e = a e + ˙ a = a a + ˙ e = a
19 12 18 raleqbidv b = B p = + ˙ a b e p a = a a p e = a a B e + ˙ a = a a + ˙ e = a
20 12 19 rexeqbidv b = B p = + ˙ e b a b e p a = a a p e = a e B a B e + ˙ a = a a + ˙ e = a
21 11 20 syl6bi g = G b = Base g p = + g e b a b e p a = a a p e = a e B a B e + ˙ a = a a + ˙ e = a
22 3 4 21 sbc2iedv g = G [˙Base g / b]˙ [˙+ g / p]˙ e b a b e p a = a a p e = a e B a B e + ˙ a = a a + ˙ e = a
23 df-mnd Could not format Mnd = { g e. Smgrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. a e. b ( ( e p a ) = a /\ ( a p e ) = a ) } : No typesetting found for |- Mnd = { g e. Smgrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. a e. b ( ( e p a ) = a /\ ( a p e ) = a ) } with typecode |-
24 22 23 elrab2 Could not format ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) ) : No typesetting found for |- ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) ) with typecode |-