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 
|- B = ( Base ` G )
lsmcomx.s 
|- .(+) = ( LSSum ` G )
Assertion lsmcomx 
|- ( ( G e. Abel /\ T C_ B /\ U C_ B ) -> ( T .(+) U ) = ( U .(+) T ) )

Proof

Step Hyp Ref Expression
1 lsmcomx.v 
 |-  B = ( Base ` G )
2 lsmcomx.s 
 |-  .(+) = ( LSSum ` G )
3 simpl1 
 |-  ( ( ( G e. Abel /\ T C_ B /\ U C_ B ) /\ ( y e. T /\ z e. U ) ) -> G e. Abel )
4 simpl2 
 |-  ( ( ( G e. Abel /\ T C_ B /\ U C_ B ) /\ ( y e. T /\ z e. U ) ) -> T C_ B )
5 simprl 
 |-  ( ( ( G e. Abel /\ T C_ B /\ U C_ B ) /\ ( y e. T /\ z e. U ) ) -> y e. T )
6 4 5 sseldd 
 |-  ( ( ( G e. Abel /\ T C_ B /\ U C_ B ) /\ ( y e. T /\ z e. U ) ) -> y e. B )
7 simpl3 
 |-  ( ( ( G e. Abel /\ T C_ B /\ U C_ B ) /\ ( y e. T /\ z e. U ) ) -> U C_ B )
8 simprr 
 |-  ( ( ( G e. Abel /\ T C_ B /\ U C_ B ) /\ ( y e. T /\ z e. U ) ) -> z e. U )
9 7 8 sseldd 
 |-  ( ( ( G e. Abel /\ T C_ B /\ U C_ B ) /\ ( y e. T /\ z e. U ) ) -> z e. B )
10 eqid 
 |-  ( +g ` G ) = ( +g ` G )
11 1 10 ablcom 
 |-  ( ( G e. Abel /\ y e. B /\ z e. B ) -> ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) )
12 3 6 9 11 syl3anc 
 |-  ( ( ( G e. Abel /\ T C_ B /\ U C_ B ) /\ ( y e. T /\ z e. U ) ) -> ( y ( +g ` G ) z ) = ( z ( +g ` G ) y ) )
13 12 eqeq2d 
 |-  ( ( ( G e. Abel /\ T C_ B /\ U C_ B ) /\ ( y e. T /\ z e. U ) ) -> ( x = ( y ( +g ` G ) z ) <-> x = ( z ( +g ` G ) y ) ) )
14 13 2rexbidva 
 |-  ( ( G e. Abel /\ T C_ B /\ U C_ B ) -> ( E. y e. T E. z e. U x = ( y ( +g ` G ) z ) <-> E. y e. T E. z e. U x = ( z ( +g ` G ) y ) ) )
15 rexcom 
 |-  ( E. y e. T E. z e. U x = ( z ( +g ` G ) y ) <-> E. z e. U E. y e. T x = ( z ( +g ` G ) y ) )
16 14 15 bitrdi 
 |-  ( ( G e. Abel /\ T C_ B /\ U C_ B ) -> ( E. y e. T E. z e. U x = ( y ( +g ` G ) z ) <-> E. z e. U E. y e. T x = ( z ( +g ` G ) y ) ) )
17 1 10 2 lsmelvalx 
 |-  ( ( G e. Abel /\ T C_ B /\ U C_ B ) -> ( x e. ( T .(+) U ) <-> E. y e. T E. z e. U x = ( y ( +g ` G ) z ) ) )
18 1 10 2 lsmelvalx 
 |-  ( ( G e. Abel /\ U C_ B /\ T C_ B ) -> ( x e. ( U .(+) T ) <-> E. z e. U E. y e. T x = ( z ( +g ` G ) y ) ) )
19 18 3com23 
 |-  ( ( G e. Abel /\ T C_ B /\ U C_ B ) -> ( x e. ( U .(+) T ) <-> E. z e. U E. y e. T x = ( z ( +g ` G ) y ) ) )
20 16 17 19 3bitr4d 
 |-  ( ( G e. Abel /\ T C_ B /\ U C_ B ) -> ( x e. ( T .(+) U ) <-> x e. ( U .(+) T ) ) )
21 20 eqrdv 
 |-  ( ( G e. Abel /\ T C_ B /\ U C_ B ) -> ( T .(+) U ) = ( U .(+) T ) )