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 ‘ 𝐺 )
Assertion grplsmid ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → ( { 𝑋 } 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 grplsmid.p = ( LSSum ‘ 𝐺 )
2 subgrcl ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
3 2 adantr ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → 𝐺 ∈ Grp )
4 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 4 subgss ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
6 5 sselda ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
7 6 snssd ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → { 𝑋 } ⊆ ( Base ‘ 𝐺 ) )
8 5 adantr ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → 𝐴 ⊆ ( Base ‘ 𝐺 ) )
9 eqid ( +g𝐺 ) = ( +g𝐺 )
10 4 9 1 lsmelvalx ( ( 𝐺 ∈ Grp ∧ { 𝑋 } ⊆ ( Base ‘ 𝐺 ) ∧ 𝐴 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑥 ∈ ( { 𝑋 } 𝐴 ) ↔ ∃ 𝑜 ∈ { 𝑋 } ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ) )
11 3 7 8 10 syl3anc ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → ( 𝑥 ∈ ( { 𝑋 } 𝐴 ) ↔ ∃ 𝑜 ∈ { 𝑋 } ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ) )
12 oveq1 ( 𝑜 = 𝑋 → ( 𝑜 ( +g𝐺 ) 𝑎 ) = ( 𝑋 ( +g𝐺 ) 𝑎 ) )
13 12 eqeq2d ( 𝑜 = 𝑋 → ( 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ↔ 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) ) )
14 13 rexbidv ( 𝑜 = 𝑋 → ( ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ↔ ∃ 𝑎𝐴 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) ) )
15 14 rexsng ( 𝑋𝐴 → ( ∃ 𝑜 ∈ { 𝑋 } ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ↔ ∃ 𝑎𝐴 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) ) )
16 15 adantl ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → ( ∃ 𝑜 ∈ { 𝑋 } ∃ 𝑎𝐴 𝑥 = ( 𝑜 ( +g𝐺 ) 𝑎 ) ↔ ∃ 𝑎𝐴 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) ) )
17 simpr ( ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑎𝐴 ) ∧ 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) ) → 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) )
18 9 subgcl ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴𝑎𝐴 ) → ( 𝑋 ( +g𝐺 ) 𝑎 ) ∈ 𝐴 )
19 18 ad4ant123 ( ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑎𝐴 ) ∧ 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) ) → ( 𝑋 ( +g𝐺 ) 𝑎 ) ∈ 𝐴 )
20 17 19 eqeltrd ( ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑎𝐴 ) ∧ 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) ) → 𝑥𝐴 )
21 20 r19.29an ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ ∃ 𝑎𝐴 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) ) → 𝑥𝐴 )
22 simpll ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑥𝐴 ) → 𝐴 ∈ ( SubGrp ‘ 𝐺 ) )
23 eqid ( invg𝐺 ) = ( invg𝐺 )
24 23 subginvcl ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → ( ( invg𝐺 ) ‘ 𝑋 ) ∈ 𝐴 )
25 24 adantr ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑥𝐴 ) → ( ( invg𝐺 ) ‘ 𝑋 ) ∈ 𝐴 )
26 simpr ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑥𝐴 ) → 𝑥𝐴 )
27 9 subgcl ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( invg𝐺 ) ‘ 𝑋 ) ∈ 𝐴𝑥𝐴 ) → ( ( ( invg𝐺 ) ‘ 𝑋 ) ( +g𝐺 ) 𝑥 ) ∈ 𝐴 )
28 22 25 26 27 syl3anc ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑥𝐴 ) → ( ( ( invg𝐺 ) ‘ 𝑋 ) ( +g𝐺 ) 𝑥 ) ∈ 𝐴 )
29 oveq2 ( 𝑎 = ( ( ( invg𝐺 ) ‘ 𝑋 ) ( +g𝐺 ) 𝑥 ) → ( 𝑋 ( +g𝐺 ) 𝑎 ) = ( 𝑋 ( +g𝐺 ) ( ( ( invg𝐺 ) ‘ 𝑋 ) ( +g𝐺 ) 𝑥 ) ) )
30 29 eqeq2d ( 𝑎 = ( ( ( invg𝐺 ) ‘ 𝑋 ) ( +g𝐺 ) 𝑥 ) → ( 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) ↔ 𝑥 = ( 𝑋 ( +g𝐺 ) ( ( ( invg𝐺 ) ‘ 𝑋 ) ( +g𝐺 ) 𝑥 ) ) ) )
31 30 adantl ( ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑥𝐴 ) ∧ 𝑎 = ( ( ( invg𝐺 ) ‘ 𝑋 ) ( +g𝐺 ) 𝑥 ) ) → ( 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) ↔ 𝑥 = ( 𝑋 ( +g𝐺 ) ( ( ( invg𝐺 ) ‘ 𝑋 ) ( +g𝐺 ) 𝑥 ) ) ) )
32 3 adantr ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑥𝐴 ) → 𝐺 ∈ Grp )
33 6 adantr ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑥𝐴 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
34 8 sselda ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑥𝐴 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
35 4 9 23 grpasscan1 ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑋 ( +g𝐺 ) ( ( ( invg𝐺 ) ‘ 𝑋 ) ( +g𝐺 ) 𝑥 ) ) = 𝑥 )
36 32 33 34 35 syl3anc ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑥𝐴 ) → ( 𝑋 ( +g𝐺 ) ( ( ( invg𝐺 ) ‘ 𝑋 ) ( +g𝐺 ) 𝑥 ) ) = 𝑥 )
37 36 eqcomd ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑥𝐴 ) → 𝑥 = ( 𝑋 ( +g𝐺 ) ( ( ( invg𝐺 ) ‘ 𝑋 ) ( +g𝐺 ) 𝑥 ) ) )
38 28 31 37 rspcedvd ( ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) ∧ 𝑥𝐴 ) → ∃ 𝑎𝐴 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) )
39 21 38 impbida ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → ( ∃ 𝑎𝐴 𝑥 = ( 𝑋 ( +g𝐺 ) 𝑎 ) ↔ 𝑥𝐴 ) )
40 11 16 39 3bitrd ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → ( 𝑥 ∈ ( { 𝑋 } 𝐴 ) ↔ 𝑥𝐴 ) )
41 40 eqrdv ( ( 𝐴 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝐴 ) → ( { 𝑋 } 𝐴 ) = 𝐴 )