copissgrp

Description: A structure with a constant group addition operation is a semigroup if the constant is contained in the base set. (Contributed by AV, 16-Feb-2020)

	Ref	Expression
Hypotheses	copissgrp.b	$⊢ B = {Base}_{M}$
	copissgrp.p	$⊢ +_{M} = (x \in B, y \in B ⟼ C)$
	copissgrp.n	$⊢ φ \to B \neq \emptyset$
	copissgrp.c	$⊢ φ \to C \in B$
Assertion	copissgrp	Could not format assertion : No typesetting found for \|- ( ph -> M e. Smgrp ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		copissgrp.b	$⊢ B = {Base}_{M}$
2		copissgrp.p	$⊢ +_{M} = (x \in B, y \in B ⟼ C)$
3		copissgrp.n	$⊢ φ \to B \neq \emptyset$
4		copissgrp.c	$⊢ φ \to C \in B$
5	4	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to C \in B$
6	1 2 3 5	opmpoismgm	$⊢ φ \to M \in Mgm$
7		eqidd	$⊢ (C \in B \land (a \in B \land b \in B \land c \in B)) \to (x \in B, y \in B ⟼ C) = (x \in B, y \in B ⟼ C)$
8		eqidd	$⊢ ((C \in B \land (a \in B \land b \in B \land c \in B)) \land (x = C \land y = c)) \to C = C$
9		simpl	$⊢ (C \in B \land (a \in B \land b \in B \land c \in B)) \to C \in B$
10		simpr3	$⊢ (C \in B \land (a \in B \land b \in B \land c \in B)) \to c \in B$
11	7 8 9 10 9	ovmpod	$⊢ (C \in B \land (a \in B \land b \in B \land c \in B)) \to C (x \in B, y \in B ⟼ C) c = C$
12		eqidd	$⊢ ((C \in B \land (a \in B \land b \in B \land c \in B)) \land (x = a \land y = C)) \to C = C$
13		simpr1	$⊢ (C \in B \land (a \in B \land b \in B \land c \in B)) \to a \in B$
14	7 12 13 9 9	ovmpod	$⊢ (C \in B \land (a \in B \land b \in B \land c \in B)) \to a (x \in B, y \in B ⟼ C) C = C$
15	11 14	eqtr4d	$⊢ (C \in B \land (a \in B \land b \in B \land c \in B)) \to C (x \in B, y \in B ⟼ C) c = a (x \in B, y \in B ⟼ C) C$
16	4 15	sylan	$⊢ (φ \land (a \in B \land b \in B \land c \in B)) \to C (x \in B, y \in B ⟼ C) c = a (x \in B, y \in B ⟼ C) C$
17		eqidd	$⊢ (φ \land (a \in B \land b \in B \land c \in B)) \to (x \in B, y \in B ⟼ C) = (x \in B, y \in B ⟼ C)$
18		eqidd	$⊢ ((φ \land (a \in B \land b \in B \land c \in B)) \land (x = a \land y = b)) \to C = C$
19		simpr1	$⊢ (φ \land (a \in B \land b \in B \land c \in B)) \to a \in B$
20		simpr2	$⊢ (φ \land (a \in B \land b \in B \land c \in B)) \to b \in B$
21	4	adantr	$⊢ (φ \land (a \in B \land b \in B \land c \in B)) \to C \in B$
22	17 18 19 20 21	ovmpod	$⊢ (φ \land (a \in B \land b \in B \land c \in B)) \to a (x \in B, y \in B ⟼ C) b = C$
23	22	oveq1d	$⊢ (φ \land (a \in B \land b \in B \land c \in B)) \to (a (x \in B, y \in B ⟼ C) b) (x \in B, y \in B ⟼ C) c = C (x \in B, y \in B ⟼ C) c$
24		eqidd	$⊢ ((φ \land (a \in B \land b \in B \land c \in B)) \land (x = b \land y = c)) \to C = C$
25		simpr3	$⊢ (φ \land (a \in B \land b \in B \land c \in B)) \to c \in B$
26	17 24 20 25 21	ovmpod	$⊢ (φ \land (a \in B \land b \in B \land c \in B)) \to b (x \in B, y \in B ⟼ C) c = C$
27	26	oveq2d	$⊢ (φ \land (a \in B \land b \in B \land c \in B)) \to a (x \in B, y \in B ⟼ C) (b (x \in B, y \in B ⟼ C) c) = a (x \in B, y \in B ⟼ C) C$
28	16 23 27	3eqtr4d	$⊢ (φ \land (a \in B \land b \in B \land c \in B)) \to (a (x \in B, y \in B ⟼ C) b) (x \in B, y \in B ⟼ C) c = a (x \in B, y \in B ⟼ C) (b (x \in B, y \in B ⟼ C) c)$
29	28	ralrimivvva	$⊢ φ \to \forall a \in B \forall b \in B \forall c \in B (a (x \in B, y \in B ⟼ C) b) (x \in B, y \in B ⟼ C) c = a (x \in B, y \in B ⟼ C) (b (x \in B, y \in B ⟼ C) c)$
30	2	eqcomi	$⊢ (x \in B, y \in B ⟼ C) = +_{M}$
31	1 30	issgrp	Could not format ( M e. Smgrp <-> ( M e. Mgm /\ A. a e. B A. b e. B A. c e. B ( ( a ( x e. B , y e. B \|-> C ) b ) ( x e. B , y e. B \|-> C ) c ) = ( a ( x e. B , y e. B \|-> C ) ( b ( x e. B , y e. B \|-> C ) c ) ) ) ) : No typesetting found for \|- ( M e. Smgrp <-> ( M e. Mgm /\ A. a e. B A. b e. B A. c e. B ( ( a ( x e. B , y e. B \|-> C ) b ) ( x e. B , y e. B \|-> C ) c ) = ( a ( x e. B , y e. B \|-> C ) ( b ( x e. B , y e. B \|-> C ) c ) ) ) ) with typecode \|-
32	6 29 31	sylanbrc	Could not format ( ph -> M e. Smgrp ) : No typesetting found for \|- ( ph -> M e. Smgrp ) with typecode \|-

Metamath Proof Explorer

Theorem copissgrp

Proof