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 ⊢ φ → M ∈ Smgrp

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 ⊢ M ∈ Smgrp ↔ M ∈ Mgm ∧ ∀ 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
32 6 29 31 sylanbrc ⊢ φ → M ∈ Smgrp