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 ∧ 𝑇𝐵𝑈𝐵 ) → ( 𝑇 𝑈 ) = ( 𝑈 𝑇 ) )