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 ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )