Theorem ismgm

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

	Ref	Expression
Hypotheses	ismgm.b	$$⊢B={\mathrm{Base}}_M$$
	ismgm.o	No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion	ismgm	Could not format assertion : No typesetting found for |- ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ismgm.b	$$⊢B={\mathrm{Base}}_M$$
2		ismgm.o	Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |-
3		fvexd	$$⊢m=M\to {\mathrm{Base}}_m\in \mathrm{V}$$
4		fveq2	$$⊢m=M\to {\mathrm{Base}}_m={\mathrm{Base}}_M$$
5	4 1	eqtr4di	$$⊢m=M\to {\mathrm{Base}}_m=B$$
6		fvexd	$$⊢\left(m=M\wedge b=B\right)\to {+}_m\in \mathrm{V}$$
7		fveq2	$$⊢m=M\to {+}_m={+}_M$$
8	7	adantr	$$⊢\left(m=M\wedge b=B\right)\to {+}_m={+}_M$$
9	8 2	eqtr4di	Could not format ( ( m = M /\ b = B ) -> ( +g ` m ) = .o. ) : No typesetting found for |- ( ( m = M /\ b = B ) -> ( +g ` m ) = .o. ) with typecode |-
10		simplr	Could not format ( ( ( m = M /\ b = B ) /\ o = .o. ) -> b = B ) : No typesetting found for |- ( ( ( m = M /\ b = B ) /\ o = .o. ) -> b = B ) with typecode |-
11		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 |-
12	11	adantl	Could not format ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( x o y ) = ( x .o. y ) ) : No typesetting found for |- ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( x o y ) = ( x .o. y ) ) with typecode |-
13	12 10	eleq12d	Could not format ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( ( x o y ) e. b <-> ( x .o. y ) e. B ) ) : No typesetting found for |- ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( ( x o y ) e. b <-> ( x .o. y ) e. B ) ) with typecode |-
14	10 13	raleqbidv	Could not format ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( A. y e. b ( x o y ) e. b <-> A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( A. y e. b ( x o y ) e. b <-> A. y e. B ( x .o. y ) e. B ) ) with typecode |-
15	10 14	raleqbidv	Could not format ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-
16	6 9 15	sbcied2	Could not format ( ( m = M /\ b = B ) -> ( [. ( +g ` m ) / o ]. A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( ( m = M /\ b = B ) -> ( [. ( +g ` m ) / o ]. A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-
17	3 5 16	sbcied2	Could not format ( m = M -> ( [. ( Base ` m ) / b ]. [. ( +g ` m ) / o ]. A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( m = M -> ( [. ( Base ` m ) / b ]. [. ( +g ` m ) / o ]. A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-
18		df-mgm	$$⊢\mathrm{Mgm}=\left\{m|\underset{\dot{}}{[}{\mathrm{Base}}_m/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_m/o\underset{\dot{}}{]}\forall x\in b\forall y\in bxoy\in b\right\}$$
19	17 18	elab2g	Could not format ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-