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