Metamath Proof Explorer

Theorem lsmcomx

Description: Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmcomx.v ⊢ 𝐵 = ( Base ‘ 𝐺 )
lsmcomx.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion lsmcomx ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 lsmcomx.v ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 lsmcomx.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
3 simpl1 ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝐺 ∈ Abel )
4 simpl2 ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑇 ⊆ 𝐵 )
5 simprl ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑇 )
6 4 5 sseldd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑦 ∈ 𝐵 )
7 simpl3 ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑈 ⊆ 𝐵 )
8 simprr ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑧 ∈ 𝑈 )
9 7 8 sseldd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑧 ∈ 𝐵 )
10 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11 1 10 ablcom ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) )
12 3 6 9 11 syl3anc ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) )
13 12 eqeq2d ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ↔ 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) )
14 13 2rexbidva ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) )
15 rexcom ⊢ ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑧 ∈ 𝑈 ∃ 𝑦 ∈ 𝑇 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) )
16 14 15 bitrdi ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ↔ ∃ 𝑧 ∈ 𝑈 ∃ 𝑦 ∈ 𝑇 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) )
17 1 10 2 lsmelvalx ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
18 1 10 2 lsmelvalx ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑈 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑈 ⊕ 𝑇 ) ↔ ∃ 𝑧 ∈ 𝑈 ∃ 𝑦 ∈ 𝑇 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) )
19 18 3com23 ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑈 ⊕ 𝑇 ) ↔ ∃ 𝑧 ∈ 𝑈 ∃ 𝑦 ∈ 𝑇 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ) )
20 16 17 19 3bitr4d ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ 𝑥 ∈ ( 𝑈 ⊕ 𝑇 ) ) )
21 20 eqrdv ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )