Metamath Proof Explorer

Theorem grplsmid

Description: The direct sum of an element X of a subgroup A is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024)

Ref Expression
Hypothesis grplsmid.p 
|- .(+) = ( LSSum ` G )
Assertion grplsmid 
|- ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> ( { X } .(+) A ) = A )

Proof

Step Hyp Ref Expression
1 grplsmid.p 
 |-  .(+) = ( LSSum ` G )
2 subgrcl 
 |-  ( A e. ( SubGrp ` G ) -> G e. Grp )
3 2 adantr 
 |-  ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> G e. Grp )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 4 subgss 
 |-  ( A e. ( SubGrp ` G ) -> A C_ ( Base ` G ) )
6 5 sselda 
 |-  ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> X e. ( Base ` G ) )
7 6 snssd 
 |-  ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> { X } C_ ( Base ` G ) )
8 5 adantr 
 |-  ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> A C_ ( Base ` G ) )
9 eqid 
 |-  ( +g ` G ) = ( +g ` G )
10 4 9 1 lsmelvalx 
 |-  ( ( G e. Grp /\ { X } C_ ( Base ` G ) /\ A C_ ( Base ` G ) ) -> ( x e. ( { X } .(+) A ) <-> E. o e. { X } E. a e. A x = ( o ( +g ` G ) a ) ) )
11 3 7 8 10 syl3anc 
 |-  ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> ( x e. ( { X } .(+) A ) <-> E. o e. { X } E. a e. A x = ( o ( +g ` G ) a ) ) )
12 oveq1 
 |-  ( o = X -> ( o ( +g ` G ) a ) = ( X ( +g ` G ) a ) )
13 12 eqeq2d 
 |-  ( o = X -> ( x = ( o ( +g ` G ) a ) <-> x = ( X ( +g ` G ) a ) ) )
14 13 rexbidv 
 |-  ( o = X -> ( E. a e. A x = ( o ( +g ` G ) a ) <-> E. a e. A x = ( X ( +g ` G ) a ) ) )
15 14 rexsng 
 |-  ( X e. A -> ( E. o e. { X } E. a e. A x = ( o ( +g ` G ) a ) <-> E. a e. A x = ( X ( +g ` G ) a ) ) )
16 15 adantl 
 |-  ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> ( E. o e. { X } E. a e. A x = ( o ( +g ` G ) a ) <-> E. a e. A x = ( X ( +g ` G ) a ) ) )
17 simpr 
 |-  ( ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ a e. A ) /\ x = ( X ( +g ` G ) a ) ) -> x = ( X ( +g ` G ) a ) )
18 9 subgcl 
 |-  ( ( A e. ( SubGrp ` G ) /\ X e. A /\ a e. A ) -> ( X ( +g ` G ) a ) e. A )
19 18 ad4ant123 
 |-  ( ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ a e. A ) /\ x = ( X ( +g ` G ) a ) ) -> ( X ( +g ` G ) a ) e. A )
20 17 19 eqeltrd 
 |-  ( ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ a e. A ) /\ x = ( X ( +g ` G ) a ) ) -> x e. A )
21 20 r19.29an 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ E. a e. A x = ( X ( +g ` G ) a ) ) -> x e. A )
22 simpll 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ x e. A ) -> A e. ( SubGrp ` G ) )
23 eqid 
 |-  ( invg ` G ) = ( invg ` G )
24 23 subginvcl 
 |-  ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> ( ( invg ` G ) ` X ) e. A )
25 24 adantr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ x e. A ) -> ( ( invg ` G ) ` X ) e. A )
26 simpr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ x e. A ) -> x e. A )
27 9 subgcl 
 |-  ( ( A e. ( SubGrp ` G ) /\ ( ( invg ` G ) ` X ) e. A /\ x e. A ) -> ( ( ( invg ` G ) ` X ) ( +g ` G ) x ) e. A )
28 22 25 26 27 syl3anc 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ x e. A ) -> ( ( ( invg ` G ) ` X ) ( +g ` G ) x ) e. A )
29 oveq2 
 |-  ( a = ( ( ( invg ` G ) ` X ) ( +g ` G ) x ) -> ( X ( +g ` G ) a ) = ( X ( +g ` G ) ( ( ( invg ` G ) ` X ) ( +g ` G ) x ) ) )
30 29 eqeq2d 
 |-  ( a = ( ( ( invg ` G ) ` X ) ( +g ` G ) x ) -> ( x = ( X ( +g ` G ) a ) <-> x = ( X ( +g ` G ) ( ( ( invg ` G ) ` X ) ( +g ` G ) x ) ) ) )
31 30 adantl 
 |-  ( ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ x e. A ) /\ a = ( ( ( invg ` G ) ` X ) ( +g ` G ) x ) ) -> ( x = ( X ( +g ` G ) a ) <-> x = ( X ( +g ` G ) ( ( ( invg ` G ) ` X ) ( +g ` G ) x ) ) ) )
32 3 adantr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ x e. A ) -> G e. Grp )
33 6 adantr 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ x e. A ) -> X e. ( Base ` G ) )
34 8 sselda 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ x e. A ) -> x e. ( Base ` G ) )
35 4 9 23 grpasscan1 
 |-  ( ( G e. Grp /\ X e. ( Base ` G ) /\ x e. ( Base ` G ) ) -> ( X ( +g ` G ) ( ( ( invg ` G ) ` X ) ( +g ` G ) x ) ) = x )
36 32 33 34 35 syl3anc 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ x e. A ) -> ( X ( +g ` G ) ( ( ( invg ` G ) ` X ) ( +g ` G ) x ) ) = x )
37 36 eqcomd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ x e. A ) -> x = ( X ( +g ` G ) ( ( ( invg ` G ) ` X ) ( +g ` G ) x ) ) )
38 28 31 37 rspcedvd 
 |-  ( ( ( A e. ( SubGrp ` G ) /\ X e. A ) /\ x e. A ) -> E. a e. A x = ( X ( +g ` G ) a ) )
39 21 38 impbida 
 |-  ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> ( E. a e. A x = ( X ( +g ` G ) a ) <-> x e. A ) )
40 11 16 39 3bitrd 
 |-  ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> ( x e. ( { X } .(+) A ) <-> x e. A ) )
41 40 eqrdv 
 |-  ( ( A e. ( SubGrp ` G ) /\ X e. A ) -> ( { X } .(+) A ) = A )