This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } ⊕ 𝐴 ) = 𝐴 )