Metamath Proof Explorer

Theorem lsmcom2

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

Ref Expression
Hypotheses lsmsubg.p 
|- .(+) = ( LSSum ` G )
lsmsubg.z 
|- Z = ( Cntz ` G )
Assertion lsmcom2 
|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) = ( U .(+) T ) )

Proof

Step Hyp Ref Expression
1 lsmsubg.p 
 |-  .(+) = ( LSSum ` G )
2 lsmsubg.z 
 |-  Z = ( Cntz ` G )
3 simp3 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> T C_ ( Z ` U ) )
4 3 sselda 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ a e. T ) -> a e. ( Z ` U ) )
5 4 adantrr 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> a e. ( Z ` U ) )
6 simprr 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> b e. U )
7 eqid 
 |-  ( +g ` G ) = ( +g ` G )
8 7 2 cntzi 
 |-  ( ( a e. ( Z ` U ) /\ b e. U ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) )
9 5 6 8 syl2anc 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( a ( +g ` G ) b ) = ( b ( +g ` G ) a ) )
10 9 eqeq2d 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) /\ ( a e. T /\ b e. U ) ) -> ( x = ( a ( +g ` G ) b ) <-> x = ( b ( +g ` G ) a ) ) )
11 10 2rexbidva 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( E. a e. T E. b e. U x = ( a ( +g ` G ) b ) <-> E. a e. T E. b e. U x = ( b ( +g ` G ) a ) ) )
12 rexcom 
 |-  ( E. a e. T E. b e. U x = ( b ( +g ` G ) a ) <-> E. b e. U E. a e. T x = ( b ( +g ` G ) a ) )
13 11 12 bitrdi 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( E. a e. T E. b e. U x = ( a ( +g ` G ) b ) <-> E. b e. U E. a e. T x = ( b ( +g ` G ) a ) ) )
14 7 1 lsmelval 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( x e. ( T .(+) U ) <-> E. a e. T E. b e. U x = ( a ( +g ` G ) b ) ) )
15 14 3adant3 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( x e. ( T .(+) U ) <-> E. a e. T E. b e. U x = ( a ( +g ` G ) b ) ) )
16 7 1 lsmelval 
 |-  ( ( U e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) -> ( x e. ( U .(+) T ) <-> E. b e. U E. a e. T x = ( b ( +g ` G ) a ) ) )
17 16 ancoms 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( x e. ( U .(+) T ) <-> E. b e. U E. a e. T x = ( b ( +g ` G ) a ) ) )
18 17 3adant3 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( x e. ( U .(+) T ) <-> E. b e. U E. a e. T x = ( b ( +g ` G ) a ) ) )
19 13 15 18 3bitr4d 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( x e. ( T .(+) U ) <-> x e. ( U .(+) T ) ) )
20 19 eqrdv 
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) /\ T C_ ( Z ` U ) ) -> ( T .(+) U ) = ( U .(+) T ) )