Metamath Proof Explorer

Theorem 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 ∈ B , y ∈ B ⟼ C
copissgrp.n ⊢ φ → B ≠ ∅
copissgrp.c ⊢ φ → C ∈ 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 ∈ B , y ∈ B ⟼ C
3 copissgrp.n ⊢ φ → B ≠ ∅
4 copissgrp.c ⊢ φ → C ∈ B
5 4 adantr ⊢ φ ∧ x ∈ B ∧ y ∈ B → C ∈ B
6 1 2 3 5 opmpoismgm ⊢ φ → M ∈ Mgm
7 eqidd ⊢ C ∈ B ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → x ∈ B , y ∈ B ⟼ C = x ∈ B , y ∈ B ⟼ C
8 eqidd ⊢ C ∈ B ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B ∧ x = C ∧ y = c → C = C
9 simpl ⊢ C ∈ B ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → C ∈ B
10 simpr3 ⊢ C ∈ B ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → c ∈ B
11 7 8 9 10 9 ovmpod ⊢ C ∈ B ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → C x ∈ B , y ∈ B ⟼ C c = C
12 eqidd ⊢ C ∈ B ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B ∧ x = a ∧ y = C → C = C
13 simpr1 ⊢ C ∈ B ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → a ∈ B
14 7 12 13 9 9 ovmpod ⊢ C ∈ B ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → a x ∈ B , y ∈ B ⟼ C C = C
15 11 14 eqtr4d ⊢ C ∈ B ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → C x ∈ B , y ∈ B ⟼ C c = a x ∈ B , y ∈ B ⟼ C C
16 4 15 sylan ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → C x ∈ B , y ∈ B ⟼ C c = a x ∈ B , y ∈ B ⟼ C C
17 eqidd ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → x ∈ B , y ∈ B ⟼ C = x ∈ B , y ∈ B ⟼ C
18 eqidd ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B ∧ x = a ∧ y = b → C = C
19 simpr1 ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → a ∈ B
20 simpr2 ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → b ∈ B
21 4 adantr ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → C ∈ B
22 17 18 19 20 21 ovmpod ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → a x ∈ B , y ∈ B ⟼ C b = C
23 22 oveq1d ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → a x ∈ B , y ∈ B ⟼ C b x ∈ B , y ∈ B ⟼ C c = C x ∈ B , y ∈ B ⟼ C c
24 eqidd ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B ∧ x = b ∧ y = c → C = C
25 simpr3 ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → c ∈ B
26 17 24 20 25 21 ovmpod ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → b x ∈ B , y ∈ B ⟼ C c = C
27 26 oveq2d ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → a x ∈ B , y ∈ B ⟼ C b x ∈ B , y ∈ B ⟼ C c = a x ∈ B , y ∈ B ⟼ C C
28 16 23 27 3eqtr4d ⊢ φ ∧ a ∈ B ∧ b ∈ B ∧ c ∈ B → a x ∈ B , y ∈ B ⟼ C b x ∈ B , y ∈ B ⟼ C c = a x ∈ B , y ∈ B ⟼ C b x ∈ B , y ∈ B ⟼ C c
29 28 ralrimivvva ⊢ φ → ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B a x ∈ B , y ∈ B ⟼ C b x ∈ B , y ∈ B ⟼ C c = a x ∈ B , y ∈ B ⟼ C b x ∈ B , y ∈ B ⟼ C c
30 2 eqcomi ⊢ x ∈ B , y ∈ 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 |-