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 ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ 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 ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U → T ⊆ Z ⁡ U
4 3 sselda ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U ∧ a ∈ T → a ∈ Z ⁡ U
5 4 adantrr ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U ∧ a ∈ T ∧ b ∈ U → a ∈ Z ⁡ U
6 simprr ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U ∧ a ∈ T ∧ b ∈ U → b ∈ U
7 eqid ⊢ + G = + G
8 7 2 cntzi ⊢ a ∈ Z ⁡ U ∧ b ∈ U → a + G b = b + G a
9 5 6 8 syl2anc ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U ∧ a ∈ T ∧ b ∈ U → a + G b = b + G a
10 9 eqeq2d ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U ∧ a ∈ T ∧ b ∈ U → x = a + G b ↔ x = b + G a
11 10 2rexbidva ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U → ∃ a ∈ T ∃ b ∈ U x = a + G b ↔ ∃ a ∈ T ∃ b ∈ U x = b + G a
12 rexcom ⊢ ∃ a ∈ T ∃ b ∈ U x = b + G a ↔ ∃ b ∈ U ∃ a ∈ T x = b + G a
13 11 12 bitrdi ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U → ∃ a ∈ T ∃ b ∈ U x = a + G b ↔ ∃ b ∈ U ∃ a ∈ T x = b + G a
14 7 1 lsmelval ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → x ∈ T ⊕ ˙ U ↔ ∃ a ∈ T ∃ b ∈ U x = a + G b
15 14 3adant3 ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U → x ∈ T ⊕ ˙ U ↔ ∃ a ∈ T ∃ b ∈ U x = a + G b
16 7 1 lsmelval ⊢ U ∈ SubGrp ⁡ G ∧ T ∈ SubGrp ⁡ G → x ∈ U ⊕ ˙ T ↔ ∃ b ∈ U ∃ a ∈ T x = b + G a
17 16 ancoms ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G → x ∈ U ⊕ ˙ T ↔ ∃ b ∈ U ∃ a ∈ T x = b + G a
18 17 3adant3 ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U → x ∈ U ⊕ ˙ T ↔ ∃ b ∈ U ∃ a ∈ T x = b + G a
19 13 15 18 3bitr4d ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U → x ∈ T ⊕ ˙ U ↔ x ∈ U ⊕ ˙ T
20 19 eqrdv ⊢ T ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ Z ⁡ U → T ⊕ ˙ U = U ⊕ ˙ T