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 ˙=LSSumG
Assertion grplsmid ASubGrpGXAX˙A=A

Proof

Step Hyp Ref Expression
1 grplsmid.p ˙=LSSumG
2 subgrcl ASubGrpGGGrp
3 2 adantr ASubGrpGXAGGrp
4 eqid BaseG=BaseG
5 4 subgss ASubGrpGABaseG
6 5 sselda ASubGrpGXAXBaseG
7 6 snssd ASubGrpGXAXBaseG
8 5 adantr ASubGrpGXAABaseG
9 eqid +G=+G
10 4 9 1 lsmelvalx GGrpXBaseGABaseGxX˙AoXaAx=o+Ga
11 3 7 8 10 syl3anc ASubGrpGXAxX˙AoXaAx=o+Ga
12 oveq1 o=Xo+Ga=X+Ga
13 12 eqeq2d o=Xx=o+Gax=X+Ga
14 13 rexbidv o=XaAx=o+GaaAx=X+Ga
15 14 rexsng XAoXaAx=o+GaaAx=X+Ga
16 15 adantl ASubGrpGXAoXaAx=o+GaaAx=X+Ga
17 simpr ASubGrpGXAaAx=X+Gax=X+Ga
18 9 subgcl ASubGrpGXAaAX+GaA
19 18 ad4ant123 ASubGrpGXAaAx=X+GaX+GaA
20 17 19 eqeltrd ASubGrpGXAaAx=X+GaxA
21 20 r19.29an ASubGrpGXAaAx=X+GaxA
22 simpll ASubGrpGXAxAASubGrpG
23 eqid invgG=invgG
24 23 subginvcl ASubGrpGXAinvgGXA
25 24 adantr ASubGrpGXAxAinvgGXA
26 simpr ASubGrpGXAxAxA
27 9 subgcl ASubGrpGinvgGXAxAinvgGX+GxA
28 22 25 26 27 syl3anc ASubGrpGXAxAinvgGX+GxA
29 oveq2 a=invgGX+GxX+Ga=X+GinvgGX+Gx
30 29 eqeq2d a=invgGX+Gxx=X+Gax=X+GinvgGX+Gx
31 30 adantl ASubGrpGXAxAa=invgGX+Gxx=X+Gax=X+GinvgGX+Gx
32 3 adantr ASubGrpGXAxAGGrp
33 6 adantr ASubGrpGXAxAXBaseG
34 8 sselda ASubGrpGXAxAxBaseG
35 4 9 23 grpasscan1 GGrpXBaseGxBaseGX+GinvgGX+Gx=x
36 32 33 34 35 syl3anc ASubGrpGXAxAX+GinvgGX+Gx=x
37 36 eqcomd ASubGrpGXAxAx=X+GinvgGX+Gx
38 28 31 37 rspcedvd ASubGrpGXAxAaAx=X+Ga
39 21 38 impbida ASubGrpGXAaAx=X+GaxA
40 11 16 39 3bitrd ASubGrpGXAxX˙AxA
41 40 eqrdv ASubGrpGXAX˙A=A