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 
|- ( +g ` M ) = ( x e. B , y e. B |-> C )
copissgrp.n 
|- ( ph -> B =/= (/) )
copissgrp.c 
|- ( ph -> C e. B )
Assertion copissgrp 
|- ( ph -> M e. Smgrp )

Proof

Step Hyp Ref Expression
1 copissgrp.b 
 |-  B = ( Base ` M )
2 copissgrp.p 
 |-  ( +g ` M ) = ( x e. B , y e. B |-> C )
3 copissgrp.n 
 |-  ( ph -> B =/= (/) )
4 copissgrp.c 
 |-  ( ph -> C e. B )
5 4 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. B )
6 1 2 3 5 opmpoismgm 
 |-  ( ph -> M e. Mgm )
7 eqidd 
 |-  ( ( C e. B /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( x e. B , y e. B |-> C ) = ( x e. B , y e. B |-> C ) )
8 eqidd 
 |-  ( ( ( C e. B /\ ( a e. B /\ b e. B /\ c e. B ) ) /\ ( x = C /\ y = c ) ) -> C = C )
9 simpl 
 |-  ( ( C e. B /\ ( a e. B /\ b e. B /\ c e. B ) ) -> C e. B )
10 simpr3 
 |-  ( ( C e. B /\ ( a e. B /\ b e. B /\ c e. B ) ) -> c e. B )
11 7 8 9 10 9 ovmpod 
 |-  ( ( C e. B /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( C ( x e. B , y e. B |-> C ) c ) = C )
12 eqidd 
 |-  ( ( ( C e. B /\ ( a e. B /\ b e. B /\ c e. B ) ) /\ ( x = a /\ y = C ) ) -> C = C )
13 simpr1 
 |-  ( ( C e. B /\ ( a e. B /\ b e. B /\ c e. B ) ) -> a e. B )
14 7 12 13 9 9 ovmpod 
 |-  ( ( C e. B /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( a ( x e. B , y e. B |-> C ) C ) = C )
15 11 14 eqtr4d 
 |-  ( ( C e. B /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( C ( x e. B , y e. B |-> C ) c ) = ( a ( x e. B , y e. B |-> C ) C ) )
16 4 15 sylan 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( C ( x e. B , y e. B |-> C ) c ) = ( a ( x e. B , y e. B |-> C ) C ) )
17 eqidd 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( x e. B , y e. B |-> C ) = ( x e. B , y e. B |-> C ) )
18 eqidd 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) /\ ( x = a /\ y = b ) ) -> C = C )
19 simpr1 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) -> a e. B )
20 simpr2 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) -> b e. B )
21 4 adantr 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) -> C e. B )
22 17 18 19 20 21 ovmpod 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( a ( x e. B , y e. B |-> C ) b ) = C )
23 22 oveq1d 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( ( a ( x e. B , y e. B |-> C ) b ) ( x e. B , y e. B |-> C ) c ) = ( C ( x e. B , y e. B |-> C ) c ) )
24 eqidd 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) /\ ( x = b /\ y = c ) ) -> C = C )
25 simpr3 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) -> c e. B )
26 17 24 20 25 21 ovmpod 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) ) -> ( b ( x e. B , y e. B |-> C ) c ) = C )
27 26 oveq2d 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ 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 ) C ) )
28 16 23 27 3eqtr4d 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ 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 ) ) )
29 28 ralrimivvva 
 |-  ( ph -> 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 ) ) )
30 2 eqcomi 
 |-  ( x e. B , y e. B |-> C ) = ( +g ` M )
31 1 30 issgrp 
 |-  ( 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 ) ) ) )
32 6 29 31 sylanbrc 
 |-  ( ph -> M e. Smgrp )