Theorem sgrp2rid2

Description: A small semigroup (with two elements) with two right identities which are different if A =/= B . (Contributed by AV, 10-Feb-2020)

	Ref	Expression
Hypotheses	mgm2nsgrp.s	|- S = { A , B }
	mgm2nsgrp.b	|- ( Base ` M ) = S
	sgrp2nmnd.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )
	sgrp2nmnd.p	|- .o. = ( +g ` M )
Assertion	sgrp2rid2	|- ( ( A e. V /\ B e. W ) -> A. x e. S A. y e. S ( y .o. x ) = y )

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	|- S = { A , B }
2		mgm2nsgrp.b	|- ( Base ` M ) = S
3		sgrp2nmnd.o	|- ( +g ` M ) = ( x e. S , y e. S |-> if ( x = A , A , B ) )
4		sgrp2nmnd.p	|- .o. = ( +g ` M )
5		prid1g	|- ( A e. V -> A e. { A , B } )
6	5 1	eleqtrrdi	|- ( A e. V -> A e. S )
7		prid2g	|- ( B e. W -> B e. { A , B } )
8	7 1	eleqtrrdi	|- ( B e. W -> B e. S )
9		simpl	|- ( ( A e. S /\ B e. S ) -> A e. S )
10	1 2 3 4	sgrp2nmndlem2	|- ( ( A e. S /\ A e. S ) -> ( A .o. A ) = A )
11	9 10	syldan	|- ( ( A e. S /\ B e. S ) -> ( A .o. A ) = A )
12		oveq1	|- ( A = B -> ( A .o. A ) = ( B .o. A ) )
13		id	|- ( A = B -> A = B )
14	12 13	eqeq12d	|- ( A = B -> ( ( A .o. A ) = A <-> ( B .o. A ) = B ) )
15	11 14	syl5ib	|- ( A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. A ) = B ) )
16		simprl	|- ( ( -. A = B /\ ( A e. S /\ B e. S ) ) -> A e. S )
17		simprr	|- ( ( -. A = B /\ ( A e. S /\ B e. S ) ) -> B e. S )
18		neqne	|- ( -. A = B -> A =/= B )
19	18	adantr	|- ( ( -. A = B /\ ( A e. S /\ B e. S ) ) -> A =/= B )
20	1 2 3 4	sgrp2nmndlem3	|- ( ( A e. S /\ B e. S /\ A =/= B ) -> ( B .o. A ) = B )
21	16 17 19 20	syl3anc	|- ( ( -. A = B /\ ( A e. S /\ B e. S ) ) -> ( B .o. A ) = B )
22	21	ex	|- ( -. A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. A ) = B ) )
23	15 22	pm2.61i	|- ( ( A e. S /\ B e. S ) -> ( B .o. A ) = B )
24	1 2 3 4	sgrp2nmndlem2	|- ( ( A e. S /\ B e. S ) -> ( A .o. B ) = A )
25	13 13	oveq12d	|- ( A = B -> ( A .o. A ) = ( B .o. B ) )
26	25 13	eqeq12d	|- ( A = B -> ( ( A .o. A ) = A <-> ( B .o. B ) = B ) )
27	11 26	syl5ib	|- ( A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. B ) = B ) )
28	1 2 3 4	sgrp2nmndlem3	|- ( ( B e. S /\ B e. S /\ A =/= B ) -> ( B .o. B ) = B )
29	17 17 19 28	syl3anc	|- ( ( -. A = B /\ ( A e. S /\ B e. S ) ) -> ( B .o. B ) = B )
30	29	ex	|- ( -. A = B -> ( ( A e. S /\ B e. S ) -> ( B .o. B ) = B ) )
31	27 30	pm2.61i	|- ( ( A e. S /\ B e. S ) -> ( B .o. B ) = B )
32	24 31	jca	|- ( ( A e. S /\ B e. S ) -> ( ( A .o. B ) = A /\ ( B .o. B ) = B ) )
33	11 23 32	jca31	|- ( ( A e. S /\ B e. S ) -> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) )
34	6 8 33	syl2an	|- ( ( A e. V /\ B e. W ) -> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) )
35	1	raleqi	|- ( A. y e. S ( y .o. x ) = y <-> A. y e. { A , B } ( y .o. x ) = y )
36		oveq1	|- ( y = A -> ( y .o. x ) = ( A .o. x ) )
37		id	|- ( y = A -> y = A )
38	36 37	eqeq12d	|- ( y = A -> ( ( y .o. x ) = y <-> ( A .o. x ) = A ) )
39		oveq1	|- ( y = B -> ( y .o. x ) = ( B .o. x ) )
40		id	|- ( y = B -> y = B )
41	39 40	eqeq12d	|- ( y = B -> ( ( y .o. x ) = y <-> ( B .o. x ) = B ) )
42	38 41	ralprg	|- ( ( A e. V /\ B e. W ) -> ( A. y e. { A , B } ( y .o. x ) = y <-> ( ( A .o. x ) = A /\ ( B .o. x ) = B ) ) )
43	35 42	syl5bb	|- ( ( A e. V /\ B e. W ) -> ( A. y e. S ( y .o. x ) = y <-> ( ( A .o. x ) = A /\ ( B .o. x ) = B ) ) )
44	43	ralbidv	|- ( ( A e. V /\ B e. W ) -> ( A. x e. S A. y e. S ( y .o. x ) = y <-> A. x e. S ( ( A .o. x ) = A /\ ( B .o. x ) = B ) ) )
45	1	raleqi	|- ( A. x e. S ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> A. x e. { A , B } ( ( A .o. x ) = A /\ ( B .o. x ) = B ) )
46		oveq2	|- ( x = A -> ( A .o. x ) = ( A .o. A ) )
47	46	eqeq1d	|- ( x = A -> ( ( A .o. x ) = A <-> ( A .o. A ) = A ) )
48		oveq2	|- ( x = A -> ( B .o. x ) = ( B .o. A ) )
49	48	eqeq1d	|- ( x = A -> ( ( B .o. x ) = B <-> ( B .o. A ) = B ) )
50	47 49	anbi12d	|- ( x = A -> ( ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( A .o. A ) = A /\ ( B .o. A ) = B ) ) )
51		oveq2	|- ( x = B -> ( A .o. x ) = ( A .o. B ) )
52	51	eqeq1d	|- ( x = B -> ( ( A .o. x ) = A <-> ( A .o. B ) = A ) )
53		oveq2	|- ( x = B -> ( B .o. x ) = ( B .o. B ) )
54	53	eqeq1d	|- ( x = B -> ( ( B .o. x ) = B <-> ( B .o. B ) = B ) )
55	52 54	anbi12d	|- ( x = B -> ( ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) )
56	50 55	ralprg	|- ( ( A e. V /\ B e. W ) -> ( A. x e. { A , B } ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) )
57	45 56	syl5bb	|- ( ( A e. V /\ B e. W ) -> ( A. x e. S ( ( A .o. x ) = A /\ ( B .o. x ) = B ) <-> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) )
58	44 57	bitrd	|- ( ( A e. V /\ B e. W ) -> ( A. x e. S A. y e. S ( y .o. x ) = y <-> ( ( ( A .o. A ) = A /\ ( B .o. A ) = B ) /\ ( ( A .o. B ) = A /\ ( B .o. B ) = B ) ) ) )
59	34 58	mpbird	|- ( ( A e. V /\ B e. W ) -> A. x e. S A. y e. S ( y .o. x ) = y )