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 ) )