Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 mgm2nsgrp.s ⊢ 𝑆 = { 𝐴 , 𝐵 }
2 mgm2nsgrp.b ⊢ ( Base ‘ 𝑀 ) = 𝑆
3 sgrp2nmnd.o ⊢ ( +g ‘ 𝑀 ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝐴 , 𝐴 , 𝐵 ) )
4 sgrp2nmnd.p ⊢ ⚬ = ( +g ‘ 𝑀 )
5 prid1g ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐵 } )
6 5 1 eleqtrrdi ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑆 )
7 prid2g ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐴 , 𝐵 } )
8 7 1 eleqtrrdi ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ 𝑆 )
9 simpl ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
10 1 2 3 4 sgrp2nmndlem2 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐴 ⚬ 𝐴 ) = 𝐴 )
11 9 10 syldan ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ⚬ 𝐴 ) = 𝐴 )
12 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ⚬ 𝐴 ) = ( 𝐵 ⚬ 𝐴 ) )
13 id ⊢ ( 𝐴 = 𝐵 → 𝐴 = 𝐵 )
14 12 13 eqeq12d ⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ⚬ 𝐴 ) = 𝐴 ↔ ( 𝐵 ⚬ 𝐴 ) = 𝐵 ) )
15 11 14 imbitrid ⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐵 ⚬ 𝐴 ) = 𝐵 ) )
16 simprl ⊢ ( ( ¬ 𝐴 = 𝐵 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → 𝐴 ∈ 𝑆 )
17 simprr ⊢ ( ( ¬ 𝐴 = 𝐵 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → 𝐵 ∈ 𝑆 )
18 neqne ⊢ ( ¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵 )
19 18 adantr ⊢ ( ( ¬ 𝐴 = 𝐵 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → 𝐴 ≠ 𝐵 )
20 1 2 3 4 sgrp2nmndlem3 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ⚬ 𝐴 ) = 𝐵 )
21 16 17 19 20 syl3anc ⊢ ( ( ¬ 𝐴 = 𝐵 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐵 ⚬ 𝐴 ) = 𝐵 )
22 21 ex ⊢ ( ¬ 𝐴 = 𝐵 → ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐵 ⚬ 𝐴 ) = 𝐵 ) )
23 15 22 pm2.61i ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐵 ⚬ 𝐴 ) = 𝐵 )
24 1 2 3 4 sgrp2nmndlem2 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ⚬ 𝐵 ) = 𝐴 )
25 13 13 oveq12d ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ⚬ 𝐴 ) = ( 𝐵 ⚬ 𝐵 ) )
26 25 13 eqeq12d ⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ⚬ 𝐴 ) = 𝐴 ↔ ( 𝐵 ⚬ 𝐵 ) = 𝐵 ) )
27 11 26 imbitrid ⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐵 ⚬ 𝐵 ) = 𝐵 ) )
28 1 2 3 4 sgrp2nmndlem3 ⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 ⚬ 𝐵 ) = 𝐵 )
29 17 17 19 28 syl3anc ⊢ ( ( ¬ 𝐴 = 𝐵 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐵 ⚬ 𝐵 ) = 𝐵 )
30 29 ex ⊢ ( ¬ 𝐴 = 𝐵 → ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐵 ⚬ 𝐵 ) = 𝐵 ) )
31 27 30 pm2.61i ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐵 ⚬ 𝐵 ) = 𝐵 )
32 24 31 jca ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 ⚬ 𝐵 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐵 ) = 𝐵 ) )
33 11 23 32 jca31 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( ( 𝐴 ⚬ 𝐴 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐴 ) = 𝐵 ) ∧ ( ( 𝐴 ⚬ 𝐵 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐵 ) = 𝐵 ) ) )
34 6 8 33 syl2an ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ( 𝐴 ⚬ 𝐴 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐴 ) = 𝐵 ) ∧ ( ( 𝐴 ⚬ 𝐵 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐵 ) = 𝐵 ) ) )
35 1 raleqi ⊢ ( ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 ↔ ∀ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑦 ⚬ 𝑥 ) = 𝑦 )
36 oveq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⚬ 𝑥 ) = ( 𝐴 ⚬ 𝑥 ) )
37 id ⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
38 36 37 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ⚬ 𝑥 ) = 𝑦 ↔ ( 𝐴 ⚬ 𝑥 ) = 𝐴 ) )
39 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ⚬ 𝑥 ) = ( 𝐵 ⚬ 𝑥 ) )
40 id ⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
41 39 40 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 ⚬ 𝑥 ) = 𝑦 ↔ ( 𝐵 ⚬ 𝑥 ) = 𝐵 ) )
42 38 41 ralprg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑦 ∈ { 𝐴 , 𝐵 } ( 𝑦 ⚬ 𝑥 ) = 𝑦 ↔ ( ( 𝐴 ⚬ 𝑥 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝑥 ) = 𝐵 ) ) )
43 35 42 bitrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 ↔ ( ( 𝐴 ⚬ 𝑥 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝑥 ) = 𝐵 ) ) )
44 43 ralbidv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 ↔ ∀ 𝑥 ∈ 𝑆 ( ( 𝐴 ⚬ 𝑥 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝑥 ) = 𝐵 ) ) )
45 1 raleqi ⊢ ( ∀ 𝑥 ∈ 𝑆 ( ( 𝐴 ⚬ 𝑥 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝑥 ) = 𝐵 ) ↔ ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ⚬ 𝑥 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝑥 ) = 𝐵 ) )
46 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐴 ⚬ 𝑥 ) = ( 𝐴 ⚬ 𝐴 ) )
47 46 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 ⚬ 𝑥 ) = 𝐴 ↔ ( 𝐴 ⚬ 𝐴 ) = 𝐴 ) )
48 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐵 ⚬ 𝑥 ) = ( 𝐵 ⚬ 𝐴 ) )
49 48 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ⚬ 𝑥 ) = 𝐵 ↔ ( 𝐵 ⚬ 𝐴 ) = 𝐵 ) )
50 47 49 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐴 ⚬ 𝑥 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝑥 ) = 𝐵 ) ↔ ( ( 𝐴 ⚬ 𝐴 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐴 ) = 𝐵 ) ) )
51 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ⚬ 𝑥 ) = ( 𝐴 ⚬ 𝐵 ) )
52 51 eqeq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ⚬ 𝑥 ) = 𝐴 ↔ ( 𝐴 ⚬ 𝐵 ) = 𝐴 ) )
53 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐵 ⚬ 𝑥 ) = ( 𝐵 ⚬ 𝐵 ) )
54 53 eqeq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐵 ⚬ 𝑥 ) = 𝐵 ↔ ( 𝐵 ⚬ 𝐵 ) = 𝐵 ) )
55 52 54 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( ( 𝐴 ⚬ 𝑥 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝑥 ) = 𝐵 ) ↔ ( ( 𝐴 ⚬ 𝐵 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐵 ) = 𝐵 ) ) )
56 50 55 ralprg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( ( 𝐴 ⚬ 𝑥 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝑥 ) = 𝐵 ) ↔ ( ( ( 𝐴 ⚬ 𝐴 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐴 ) = 𝐵 ) ∧ ( ( 𝐴 ⚬ 𝐵 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐵 ) = 𝐵 ) ) ) )
57 45 56 bitrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ 𝑆 ( ( 𝐴 ⚬ 𝑥 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝑥 ) = 𝐵 ) ↔ ( ( ( 𝐴 ⚬ 𝐴 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐴 ) = 𝐵 ) ∧ ( ( 𝐴 ⚬ 𝐵 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐵 ) = 𝐵 ) ) ) )
58 44 57 bitrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 ↔ ( ( ( 𝐴 ⚬ 𝐴 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐴 ) = 𝐵 ) ∧ ( ( 𝐴 ⚬ 𝐵 ) = 𝐴 ∧ ( 𝐵 ⚬ 𝐵 ) = 𝐵 ) ) ) )
59 34 58 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑦 ⚬ 𝑥 ) = 𝑦 )