Metamath Proof Explorer

Theorem sgrp2rid2ex

Description: A small semigroup (with two elements) with two right identities which are different. (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 sgrp2rid2ex 
|- ( ( # ` S ) = 2 -> E. x e. S E. z e. S A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = 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 1 hashprdifel 
 |-  ( ( # ` S ) = 2 -> ( A e. S /\ B e. S /\ A =/= B ) )
6 simp1 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> A e. S )
7 simp2 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> B e. S )
8 simpl3 
 |-  ( ( ( A e. S /\ B e. S /\ A =/= B ) /\ y e. S ) -> A =/= B )
9 8 ralrimiva 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> A. y e. S A =/= B )
10 1 2 3 4 sgrp2rid2 
 |-  ( ( A e. S /\ B e. S ) -> A. x e. S A. y e. S ( y .o. x ) = y )
11 oveq2 
 |-  ( x = A -> ( y .o. x ) = ( y .o. A ) )
12 11 eqeq1d 
 |-  ( x = A -> ( ( y .o. x ) = y <-> ( y .o. A ) = y ) )
13 12 ralbidv 
 |-  ( x = A -> ( A. y e. S ( y .o. x ) = y <-> A. y e. S ( y .o. A ) = y ) )
14 13 rspcv 
 |-  ( A e. S -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. A ) = y ) )
15 14 adantr 
 |-  ( ( A e. S /\ B e. S ) -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. A ) = y ) )
16 10 15 mpd 
 |-  ( ( A e. S /\ B e. S ) -> A. y e. S ( y .o. A ) = y )
17 16 3adant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> A. y e. S ( y .o. A ) = y )
18 oveq2 
 |-  ( x = B -> ( y .o. x ) = ( y .o. B ) )
19 18 eqeq1d 
 |-  ( x = B -> ( ( y .o. x ) = y <-> ( y .o. B ) = y ) )
20 19 ralbidv 
 |-  ( x = B -> ( A. y e. S ( y .o. x ) = y <-> A. y e. S ( y .o. B ) = y ) )
21 20 rspcv 
 |-  ( B e. S -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. B ) = y ) )
22 21 adantl 
 |-  ( ( A e. S /\ B e. S ) -> ( A. x e. S A. y e. S ( y .o. x ) = y -> A. y e. S ( y .o. B ) = y ) )
23 10 22 mpd 
 |-  ( ( A e. S /\ B e. S ) -> A. y e. S ( y .o. B ) = y )
24 23 3adant3 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> A. y e. S ( y .o. B ) = y )
25 r19.26-3 
 |-  ( A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) <-> ( A. y e. S A =/= B /\ A. y e. S ( y .o. A ) = y /\ A. y e. S ( y .o. B ) = y ) )
26 9 17 24 25 syl3anbrc 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) )
27 6 7 26 3jca 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( A e. S /\ B e. S /\ A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) )
28 neeq1 
 |-  ( x = A -> ( x =/= z <-> A =/= z ) )
29 biidd 
 |-  ( x = A -> ( ( y .o. z ) = y <-> ( y .o. z ) = y ) )
30 28 12 29 3anbi123d 
 |-  ( x = A -> ( ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) <-> ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) ) )
31 30 ralbidv 
 |-  ( x = A -> ( A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) <-> A. y e. S ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) ) )
32 neeq2 
 |-  ( z = B -> ( A =/= z <-> A =/= B ) )
33 biidd 
 |-  ( z = B -> ( ( y .o. A ) = y <-> ( y .o. A ) = y ) )
34 oveq2 
 |-  ( z = B -> ( y .o. z ) = ( y .o. B ) )
35 34 eqeq1d 
 |-  ( z = B -> ( ( y .o. z ) = y <-> ( y .o. B ) = y ) )
36 32 33 35 3anbi123d 
 |-  ( z = B -> ( ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) <-> ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) )
37 36 ralbidv 
 |-  ( z = B -> ( A. y e. S ( A =/= z /\ ( y .o. A ) = y /\ ( y .o. z ) = y ) <-> A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) )
38 31 37 rspc2ev 
 |-  ( ( A e. S /\ B e. S /\ A. y e. S ( A =/= B /\ ( y .o. A ) = y /\ ( y .o. B ) = y ) ) -> E. x e. S E. z e. S A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) )
39 5 27 38 3syl 
 |-  ( ( # ` S ) = 2 -> E. x e. S E. z e. S A. y e. S ( x =/= z /\ ( y .o. x ) = y /\ ( y .o. z ) = y ) )