Metamath Proof Explorer


Theorem grplsm0l

Description: Sumset with the identity singleton is the original set. (Contributed by Thierry Arnoux, 27-Jul-2024)

Ref Expression
Hypotheses grplsm0l.b 𝐵 = ( Base ‘ 𝐺 )
grplsm0l.p = ( LSSum ‘ 𝐺 )
grplsm0l.0 0 = ( 0g𝐺 )
Assertion grplsm0l ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) → ( { 0 } 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 grplsm0l.b 𝐵 = ( Base ‘ 𝐺 )
2 grplsm0l.p = ( LSSum ‘ 𝐺 )
3 grplsm0l.0 0 = ( 0g𝐺 )
4 1 3 grpidcl ( 𝐺 ∈ Grp → 0𝐵 )
5 4 snssd ( 𝐺 ∈ Grp → { 0 } ⊆ 𝐵 )
6 eqid ( +g𝐺 ) = ( +g𝐺 )
7 1 6 2 lsmelvalx ( ( 𝐺 ∈ Grp ∧ { 0 } ⊆ 𝐵𝐴𝐵 ) → ( 𝑥 ∈ ( { 0 } 𝐴 ) ↔ ∃ 𝑜 ∈ { 0 } ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ) )
8 7 3expa ( ( ( 𝐺 ∈ Grp ∧ { 0 } ⊆ 𝐵 ) ∧ 𝐴𝐵 ) → ( 𝑥 ∈ ( { 0 } 𝐴 ) ↔ ∃ 𝑜 ∈ { 0 } ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ) )
9 8 an32s ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵 ) ∧ { 0 } ⊆ 𝐵 ) → ( 𝑥 ∈ ( { 0 } 𝐴 ) ↔ ∃ 𝑜 ∈ { 0 } ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ) )
10 5 9 mpidan ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵 ) → ( 𝑥 ∈ ( { 0 } 𝐴 ) ↔ ∃ 𝑜 ∈ { 0 } ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ) )
11 10 3adant3 ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) → ( 𝑥 ∈ ( { 0 } 𝐴 ) ↔ ∃ 𝑜 ∈ { 0 } ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ) )
12 simpl1 ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) ∧ 𝑎𝐴 ) → 𝐺 ∈ Grp )
13 simp2 ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) → 𝐴𝐵 )
14 13 sselda ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) ∧ 𝑎𝐴 ) → 𝑎𝐵 )
15 1 6 3 grplid ( ( 𝐺 ∈ Grp ∧ 𝑎𝐵 ) → ( 0 ( +g𝐺 ) 𝑎 ) = 𝑎 )
16 12 14 15 syl2anc ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) ∧ 𝑎𝐴 ) → ( 0 ( +g𝐺 ) 𝑎 ) = 𝑎 )
17 16 eqeq2d ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) ∧ 𝑎𝐴 ) → ( 𝑥 = ( 0 ( +g𝐺 ) 𝑎 ) ↔ 𝑥 = 𝑎 ) )
18 equcom ( 𝑥 = 𝑎𝑎 = 𝑥 )
19 17 18 bitrdi ( ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) ∧ 𝑎𝐴 ) → ( 𝑥 = ( 0 ( +g𝐺 ) 𝑎 ) ↔ 𝑎 = 𝑥 ) )
20 19 rexbidva ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) → ( ∃ 𝑎𝐴 𝑥 = ( 0 ( +g𝐺 ) 𝑎 ) ↔ ∃ 𝑎𝐴 𝑎 = 𝑥 ) )
21 3 fvexi 0 ∈ V
22 oveq1 ( 𝑜 = 0 → ( 𝑜 ( +g𝐺 ) 𝑎 ) = ( 0 ( +g𝐺 ) 𝑎 ) )
23 22 eqeq2d ( 𝑜 = 0 → ( 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ↔ 𝑥 = ( 0 ( +g𝐺 ) 𝑎 ) ) )
24 23 rexbidv ( 𝑜 = 0 → ( ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ↔ ∃ 𝑎𝐴 𝑥 = ( 0 ( +g𝐺 ) 𝑎 ) ) )
25 21 24 rexsn ( ∃ 𝑜 ∈ { 0 } ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ↔ ∃ 𝑎𝐴 𝑥 = ( 0 ( +g𝐺 ) 𝑎 ) )
26 risset ( 𝑥𝐴 ↔ ∃ 𝑎𝐴 𝑎 = 𝑥 )
27 20 25 26 3bitr4g ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) → ( ∃ 𝑜 ∈ { 0 } ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ↔ 𝑥𝐴 ) )
28 11 27 bitrd ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) → ( 𝑥 ∈ ( { 0 } 𝐴 ) ↔ 𝑥𝐴 ) )
29 28 eqrdv ( ( 𝐺 ∈ Grp ∧ 𝐴𝐵𝐴 ≠ ∅ ) → ( { 0 } 𝐴 ) = 𝐴 )