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	⊢ 𝑆 = { 𝐴 , 𝐵 }
	mgm2nsgrp.b	⊢ ( Base ‘ 𝑀 ) = 𝑆
	sgrp2nmnd.o	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) )
	sgrp2nmnd.p	⊢ ⚬ = ( +g ‘ 𝑀 )
Assertion	sgrp2rid2ex	⊢ ( ( ♯ ‘ 𝑆 ) = 2 → ∃ 𝑥 ∈ 𝑆 ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ≠ 𝑧 ∧ ( 𝑦 ⚬ 𝑥 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝑧 ) = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	⊢ 𝑆 = { 𝐴 , 𝐵 }
2		mgm2nsgrp.b	⊢ ( Base ‘ 𝑀 ) = 𝑆
3		sgrp2nmnd.o	⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) )
4		sgrp2nmnd.p	⊢ ⚬ = ( +g ‘ 𝑀 )
5	1	hashprdifel	⊢ ( ( ♯ ‘ 𝑆 ) = 2 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) )
6		simp1	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑆 )
7		simp2	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑆 )
8		simpl3	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐴 ≠ 𝐵 )
9	8	ralrimiva	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑦 ∈ 𝑆 𝐴 ≠ 𝐵 )
10	1 2 3 4	sgrp2rid2	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 )
11		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑦 ⚬ 𝑥 ) = ( 𝑦 ⚬ 𝐴 ) )
12	11	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ⚬ 𝑥 ) = 𝑦 ↔ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ) )
13	12	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐴 ) = 𝑦 ) )
14	13	rspcv	⊢ ( 𝐴 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 → ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐴 ) = 𝑦 ) )
15	14	adantr	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 → ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐴 ) = 𝑦 ) )
16	10 15	mpd	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐴 ) = 𝑦 )
17	16	3adant3	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐴 ) = 𝑦 )
18		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝑦 ⚬ 𝑥 ) = ( 𝑦 ⚬ 𝐵 ) )
19	18	eqeq1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑦 ⚬ 𝑥 ) = 𝑦 ↔ ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) )
20	19	ralbidv	⊢ ( 𝑥 = 𝐵 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) )
21	20	rspcv	⊢ ( 𝐵 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 → ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) )
22	21	adantl	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 → ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) )
23	10 22	mpd	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐵 ) = 𝑦 )
24	23	3adant3	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐵 ) = 𝑦 )
25		r19.26-3	⊢ ( ∀ 𝑦 ∈ 𝑆 ( 𝐴 ≠ 𝐵 ∧ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝐴 ≠ 𝐵 ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐴 ) = 𝑦 ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) )
26	9 17 24 25	syl3anbrc	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑦 ∈ 𝑆 ( 𝐴 ≠ 𝐵 ∧ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) )
27	6 7 26	3jca	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( 𝐴 ≠ 𝐵 ∧ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) ) )
28		neeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≠ 𝑧 ↔ 𝐴 ≠ 𝑧 ) )
29		biidd	⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ⚬ 𝑧 ) = 𝑦 ↔ ( 𝑦 ⚬ 𝑧 ) = 𝑦 ) )
30	28 12 29	3anbi123d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≠ 𝑧 ∧ ( 𝑦 ⚬ 𝑥 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝑧 ) = 𝑦 ) ↔ ( 𝐴 ≠ 𝑧 ∧ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝑧 ) = 𝑦 ) ) )
31	30	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ≠ 𝑧 ∧ ( 𝑦 ⚬ 𝑥 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝑧 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝐴 ≠ 𝑧 ∧ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝑧 ) = 𝑦 ) ) )
32		neeq2	⊢ ( 𝑧 = 𝐵 → ( 𝐴 ≠ 𝑧 ↔ 𝐴 ≠ 𝐵 ) )
33		biidd	⊢ ( 𝑧 = 𝐵 → ( ( 𝑦 ⚬ 𝐴 ) = 𝑦 ↔ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ) )
34		oveq2	⊢ ( 𝑧 = 𝐵 → ( 𝑦 ⚬ 𝑧 ) = ( 𝑦 ⚬ 𝐵 ) )
35	34	eqeq1d	⊢ ( 𝑧 = 𝐵 → ( ( 𝑦 ⚬ 𝑧 ) = 𝑦 ↔ ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) )
36	32 33 35	3anbi123d	⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ≠ 𝑧 ∧ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝑧 ) = 𝑦 ) ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) ) )
37	36	ralbidv	⊢ ( 𝑧 = 𝐵 → ( ∀ 𝑦 ∈ 𝑆 ( 𝐴 ≠ 𝑧 ∧ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝑧 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝐴 ≠ 𝐵 ∧ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) ) )
38	31 37	rspc2ev	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( 𝐴 ≠ 𝐵 ∧ ( 𝑦 ⚬ 𝐴 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝐵 ) = 𝑦 ) ) → ∃ 𝑥 ∈ 𝑆 ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ≠ 𝑧 ∧ ( 𝑦 ⚬ 𝑥 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝑧 ) = 𝑦 ) )
39	5 27 38	3syl	⊢ ( ( ♯ ‘ 𝑆 ) = 2 → ∃ 𝑥 ∈ 𝑆 ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ≠ 𝑧 ∧ ( 𝑦 ⚬ 𝑥 ) = 𝑦 ∧ ( 𝑦 ⚬ 𝑧 ) = 𝑦 ) )