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 SubGrp G X A X ˙ A = A

Proof

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