Metamath Proof Explorer


Theorem lsmcom2

Description: Subgroup sum commutes. (Contributed by Mario Carneiro, 22-Apr-2016)

Ref Expression
Hypotheses lsmsubg.p = ( LSSum ‘ 𝐺 )
lsmsubg.z 𝑍 = ( Cntz ‘ 𝐺 )
Assertion lsmcom2 ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) → ( 𝑇 𝑈 ) = ( 𝑈 𝑇 ) )

Proof

Step Hyp Ref Expression
1 lsmsubg.p = ( LSSum ‘ 𝐺 )
2 lsmsubg.z 𝑍 = ( Cntz ‘ 𝐺 )
3 simp3 ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) → 𝑇 ⊆ ( 𝑍𝑈 ) )
4 3 sselda ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) ∧ 𝑎𝑇 ) → 𝑎 ∈ ( 𝑍𝑈 ) )
5 4 adantrr ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) ∧ ( 𝑎𝑇𝑏𝑈 ) ) → 𝑎 ∈ ( 𝑍𝑈 ) )
6 simprr ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) ∧ ( 𝑎𝑇𝑏𝑈 ) ) → 𝑏𝑈 )
7 eqid ( +g𝐺 ) = ( +g𝐺 )
8 7 2 cntzi ( ( 𝑎 ∈ ( 𝑍𝑈 ) ∧ 𝑏𝑈 ) → ( 𝑎 ( +g𝐺 ) 𝑏 ) = ( 𝑏 ( +g𝐺 ) 𝑎 ) )
9 5 6 8 syl2anc ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) ∧ ( 𝑎𝑇𝑏𝑈 ) ) → ( 𝑎 ( +g𝐺 ) 𝑏 ) = ( 𝑏 ( +g𝐺 ) 𝑎 ) )
10 9 eqeq2d ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) ∧ ( 𝑎𝑇𝑏𝑈 ) ) → ( 𝑥 = ( 𝑎 ( +g𝐺 ) 𝑏 ) ↔ 𝑥 = ( 𝑏 ( +g𝐺 ) 𝑎 ) ) )
11 10 2rexbidva ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) → ( ∃ 𝑎𝑇𝑏𝑈 𝑥 = ( 𝑎 ( +g𝐺 ) 𝑏 ) ↔ ∃ 𝑎𝑇𝑏𝑈 𝑥 = ( 𝑏 ( +g𝐺 ) 𝑎 ) ) )
12 rexcom ( ∃ 𝑎𝑇𝑏𝑈 𝑥 = ( 𝑏 ( +g𝐺 ) 𝑎 ) ↔ ∃ 𝑏𝑈𝑎𝑇 𝑥 = ( 𝑏 ( +g𝐺 ) 𝑎 ) )
13 11 12 bitrdi ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) → ( ∃ 𝑎𝑇𝑏𝑈 𝑥 = ( 𝑎 ( +g𝐺 ) 𝑏 ) ↔ ∃ 𝑏𝑈𝑎𝑇 𝑥 = ( 𝑏 ( +g𝐺 ) 𝑎 ) ) )
14 7 1 lsmelval ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑇 𝑈 ) ↔ ∃ 𝑎𝑇𝑏𝑈 𝑥 = ( 𝑎 ( +g𝐺 ) 𝑏 ) ) )
15 14 3adant3 ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) → ( 𝑥 ∈ ( 𝑇 𝑈 ) ↔ ∃ 𝑎𝑇𝑏𝑈 𝑥 = ( 𝑎 ( +g𝐺 ) 𝑏 ) ) )
16 7 1 lsmelval ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑈 𝑇 ) ↔ ∃ 𝑏𝑈𝑎𝑇 𝑥 = ( 𝑏 ( +g𝐺 ) 𝑎 ) ) )
17 16 ancoms ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑈 𝑇 ) ↔ ∃ 𝑏𝑈𝑎𝑇 𝑥 = ( 𝑏 ( +g𝐺 ) 𝑎 ) ) )
18 17 3adant3 ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) → ( 𝑥 ∈ ( 𝑈 𝑇 ) ↔ ∃ 𝑏𝑈𝑎𝑇 𝑥 = ( 𝑏 ( +g𝐺 ) 𝑎 ) ) )
19 13 15 18 3bitr4d ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) → ( 𝑥 ∈ ( 𝑇 𝑈 ) ↔ 𝑥 ∈ ( 𝑈 𝑇 ) ) )
20 19 eqrdv ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍𝑈 ) ) → ( 𝑇 𝑈 ) = ( 𝑈 𝑇 ) )