This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {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 = {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 {Base}_{m} \in V$
4		fveq2	$⊢ m = M \to {Base}_{m} = {Base}_{M}$
5	4 1	eqtr4di	$⊢ m = M \to {Base}_{m} = B$
6		fvexd	$⊢ (m = M \land b = B) \to +_{m} \in V$
7		fveq2	$⊢ m = M \to +_{m} = +_{M}$
8	7	adantr	$⊢ (m = M \land b = B) \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	$⊢ Mgm = \{m \| \underset{˙}{[} {Base}_{m} / b \underset{˙}{]} \underset{˙}{[} +_{m} / o \underset{˙}{]} \forall x \in b \forall y \in b x o y \in b\}$
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 \|-