Metamath Proof Explorer


Theorem elgrplsmsn

Description: Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024)

Ref Expression
Hypotheses elgrplsmsn.1 B = Base G
elgrplsmsn.2 + ˙ = + G
elgrplsmsn.3 ˙ = LSSum G
elgrplsmsn.4 φ G V
elgrplsmsn.5 φ A B
elgrplsmsn.6 φ X B
Assertion elgrplsmsn φ Z A ˙ X x A Z = x + ˙ X

Proof

Step Hyp Ref Expression
1 elgrplsmsn.1 B = Base G
2 elgrplsmsn.2 + ˙ = + G
3 elgrplsmsn.3 ˙ = LSSum G
4 elgrplsmsn.4 φ G V
5 elgrplsmsn.5 φ A B
6 elgrplsmsn.6 φ X B
7 6 snssd φ X B
8 1 2 3 lsmelvalx G V A B X B Z A ˙ X x A y X Z = x + ˙ y
9 4 5 7 8 syl3anc φ Z A ˙ X x A y X Z = x + ˙ y
10 oveq2 y = X x + ˙ y = x + ˙ X
11 10 eqeq2d y = X Z = x + ˙ y Z = x + ˙ X
12 11 rexsng X B y X Z = x + ˙ y Z = x + ˙ X
13 6 12 syl φ y X Z = x + ˙ y Z = x + ˙ X
14 13 rexbidv φ x A y X Z = x + ˙ y x A Z = x + ˙ X
15 9 14 bitrd φ Z A ˙ X x A Z = x + ˙ X