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

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 ` G )
elgrplsmsn.3 
|- .(+) = ( LSSum ` G )
elgrplsmsn.4 
|- ( ph -> G e. V )
elgrplsmsn.5 
|- ( ph -> A C_ B )
elgrplsmsn.6 
|- ( ph -> X e. B )
Assertion elgrplsmsn 
|- ( ph -> ( Z e. ( A .(+) { X } ) <-> E. x e. A Z = ( x .+ X ) ) )

Proof

Step Hyp Ref Expression
1 elgrplsmsn.1 
 |-  B = ( Base ` G )
2 elgrplsmsn.2 
 |-  .+ = ( +g ` G )
3 elgrplsmsn.3 
 |-  .(+) = ( LSSum ` G )
4 elgrplsmsn.4 
 |-  ( ph -> G e. V )
5 elgrplsmsn.5 
 |-  ( ph -> A C_ B )
6 elgrplsmsn.6 
 |-  ( ph -> X e. B )
7 6 snssd 
 |-  ( ph -> { X } C_ B )
8 1 2 3 lsmelvalx 
 |-  ( ( G e. V /\ A C_ B /\ { X } C_ B ) -> ( Z e. ( A .(+) { X } ) <-> E. x e. A E. y e. { X } Z = ( x .+ y ) ) )
9 4 5 7 8 syl3anc 
 |-  ( ph -> ( Z e. ( A .(+) { X } ) <-> E. x e. A E. y e. { 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 e. B -> ( E. y e. { X } Z = ( x .+ y ) <-> Z = ( x .+ X ) ) )
13 6 12 syl 
 |-  ( ph -> ( E. y e. { X } Z = ( x .+ y ) <-> Z = ( x .+ X ) ) )
14 13 rexbidv 
 |-  ( ph -> ( E. x e. A E. y e. { X } Z = ( x .+ y ) <-> E. x e. A Z = ( x .+ X ) ) )
15 9 14 bitrd 
 |-  ( ph -> ( Z e. ( A .(+) { X } ) <-> E. x e. A Z = ( x .+ X ) ) )