Metamath Proof Explorer

Theorem lsmsubg

Description: The sum of two commuting subgroups is a subgroup. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmsubg.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
lsmsubg.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
Assertion lsmsubg ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 lsmsubg.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
2 lsmsubg.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
3 simp1 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
4 subgsubm ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ∈ ( SubMnd ‘ 𝐺 ) )
5 3 4 syl ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → 𝑇 ∈ ( SubMnd ‘ 𝐺 ) )
6 simp2 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
7 subgsubm ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ∈ ( SubMnd ‘ 𝐺 ) )
8 6 7 syl ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → 𝑈 ∈ ( SubMnd ‘ 𝐺 ) )
9 simp3 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
10 1 2 lsmsubm ⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑇 ⊕ 𝑈 ) ∈ ( SubMnd ‘ 𝐺 ) )
11 5 8 9 10 syl3anc ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑇 ⊕ 𝑈 ) ∈ ( SubMnd ‘ 𝐺 ) )
12 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
13 12 1 lsmelval ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑎 ∈ 𝑇 ∃ 𝑏 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) )
14 13 3adant3 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑎 ∈ 𝑇 ∃ 𝑏 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) )
15 3 adantr ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
16 subgrcl ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
17 15 16 syl ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → 𝐺 ∈ Grp )
18 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
19 18 subgss ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
20 15 19 syl ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
21 simprl ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑎 ∈ 𝑇 )
22 20 21 sseldd ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑎 ∈ ( Base ‘ 𝐺 ) )
23 6 adantr ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
24 18 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
25 23 24 syl ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
26 simprr ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑏 ∈ 𝑈 )
27 25 26 sseldd ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑏 ∈ ( Base ‘ 𝐺 ) )
28 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
29 18 12 28 grpinvadd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ ( Base ‘ 𝐺 ) ∧ 𝑏 ∈ ( Base ‘ 𝐺 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ) )
30 17 22 27 29 syl3anc ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ) )
31 9 adantr ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
32 28 subginvcl ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑎 ∈ 𝑇 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑇 )
33 15 21 32 syl2anc ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑇 )
34 31 33 sseldd ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ ( 𝑍 ‘ 𝑈 ) )
35 28 subginvcl ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑏 ∈ 𝑈 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ∈ 𝑈 )
36 23 26 35 syl2anc ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ∈ 𝑈 )
37 12 2 cntzi ⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ ( 𝑍 ‘ 𝑈 ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ∈ 𝑈 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ) )
38 34 36 37 syl2anc ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ) )
39 30 38 eqtr4d ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ) )
40 12 1 lsmelvali ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ∈ 𝑇 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ∈ 𝑈 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) )
41 15 23 33 36 40 syl22anc ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑏 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) )
42 39 41 eqeltrd ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) )
43 fveq2 ⊢ ( 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) )
44 43 eleq1d ⊢ ( 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ( ( invg ‘ 𝐺 ) ‘ ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) ) )
45 42 44 syl5ibrcom ⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) )
46 45 rexlimdvva ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( ∃ 𝑎 ∈ 𝑇 ∃ 𝑏 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) )
47 14 46 sylbid ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) )
48 47 ralrimiv ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ∀ 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑇 ⊕ 𝑈 ) )
49 3 16 syl ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → 𝐺 ∈ Grp )
50 28 issubg3 ⊢ ( 𝐺 ∈ Grp → ( ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ( 𝑇 ⊕ 𝑈 ) ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) )
51 49 50 syl ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ( 𝑇 ⊕ 𝑈 ) ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) )
52 11 48 51 mpbir2and ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝐺 ) )