lsmsubg

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

	Ref	Expression
Hypotheses	lsmsubg.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	lsmsubg.z	$⊢ Z = Cntz (G)$
Assertion	lsmsubg	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U \in SubGrp (G)$

Proof

Step	Hyp	Ref	Expression
1		lsmsubg.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		lsmsubg.z	$⊢ Z = Cntz (G)$
3		simp1	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \in SubGrp (G)$
4		subgsubm	$⊢ T \in SubGrp (G) \to T \in SubMnd (G)$
5	3 4	syl	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \in SubMnd (G)$
6		simp2	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to U \in SubGrp (G)$
7		subgsubm	$⊢ U \in SubGrp (G) \to U \in SubMnd (G)$
8	6 7	syl	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to U \in SubMnd (G)$
9		simp3	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \subseteq Z (U)$
10	1 2	lsmsubm	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U \in SubMnd (G)$
11	5 8 9 10	syl3anc	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U \in SubMnd (G)$
12		eqid	$⊢ +_{G} = +_{G}$
13	12 1	lsmelval	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists a \in T \exists b \in U x = a +_{G} b)$
14	13	3adant3	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists a \in T \exists b \in U x = a +_{G} b)$
15	3	adantr	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to T \in SubGrp (G)$
16		subgrcl	$⊢ T \in SubGrp (G) \to G \in Grp$
17	15 16	syl	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to G \in Grp$
18		eqid	$⊢ {Base}_{G} = {Base}_{G}$
19	18	subgss	$⊢ T \in SubGrp (G) \to T \subseteq {Base}_{G}$
20	15 19	syl	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to T \subseteq {Base}_{G}$
21		simprl	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to a \in T$
22	20 21	sseldd	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to a \in {Base}_{G}$
23	6	adantr	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to U \in SubGrp (G)$
24	18	subgss	$⊢ U \in SubGrp (G) \to U \subseteq {Base}_{G}$
25	23 24	syl	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to U \subseteq {Base}_{G}$
26		simprr	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to b \in U$
27	25 26	sseldd	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to b \in {Base}_{G}$
28		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
29	18 12 28	grpinvadd	$⊢ (G \in Grp \land a \in {Base}_{G} \land b \in {Base}_{G}) \to {inv}_{g} (G) (a +_{G} b) = {inv}_{g} (G) (b) +_{G} {inv}_{g} (G) (a)$
30	17 22 27 29	syl3anc	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to {inv}_{g} (G) (a +_{G} b) = {inv}_{g} (G) (b) +_{G} {inv}_{g} (G) (a)$
31	9	adantr	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to T \subseteq Z (U)$
32	28	subginvcl	$⊢ (T \in SubGrp (G) \land a \in T) \to {inv}_{g} (G) (a) \in T$
33	15 21 32	syl2anc	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to {inv}_{g} (G) (a) \in T$
34	31 33	sseldd	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to {inv}_{g} (G) (a) \in Z (U)$
35	28	subginvcl	$⊢ (U \in SubGrp (G) \land b \in U) \to {inv}_{g} (G) (b) \in U$
36	23 26 35	syl2anc	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to {inv}_{g} (G) (b) \in U$
37	12 2	cntzi	$⊢ ({inv}_{g} (G) (a) \in Z (U) \land {inv}_{g} (G) (b) \in U) \to {inv}_{g} (G) (a) +_{G} {inv}_{g} (G) (b) = {inv}_{g} (G) (b) +_{G} {inv}_{g} (G) (a)$
38	34 36 37	syl2anc	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to {inv}_{g} (G) (a) +_{G} {inv}_{g} (G) (b) = {inv}_{g} (G) (b) +_{G} {inv}_{g} (G) (a)$
39	30 38	eqtr4d	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to {inv}_{g} (G) (a +_{G} b) = {inv}_{g} (G) (a) +_{G} {inv}_{g} (G) (b)$
40	12 1	lsmelvali	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G)) \land ({inv}_{g} (G) (a) \in T \land {inv}_{g} (G) (b) \in U)) \to {inv}_{g} (G) (a) +_{G} {inv}_{g} (G) (b) \in (T \underset{˙}{\oplus} U)$
41	15 23 33 36 40	syl22anc	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to {inv}_{g} (G) (a) +_{G} {inv}_{g} (G) (b) \in (T \underset{˙}{\oplus} U)$
42	39 41	eqeltrd	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to {inv}_{g} (G) (a +_{G} b) \in (T \underset{˙}{\oplus} U)$
43		fveq2	$⊢ x = a +_{G} b \to {inv}_{g} (G) (x) = {inv}_{g} (G) (a +_{G} b)$
44	43	eleq1d	$⊢ x = a +_{G} b \to ({inv}_{g} (G) (x) \in (T \underset{˙}{\oplus} U) \leftrightarrow {inv}_{g} (G) (a +_{G} b) \in (T \underset{˙}{\oplus} U))$
45	42 44	syl5ibrcom	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to (x = a +_{G} b \to {inv}_{g} (G) (x) \in (T \underset{˙}{\oplus} U))$
46	45	rexlimdvva	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to (\exists a \in T \exists b \in U x = a +_{G} b \to {inv}_{g} (G) (x) \in (T \underset{˙}{\oplus} U))$
47	14 46	sylbid	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to (x \in (T \underset{˙}{\oplus} U) \to {inv}_{g} (G) (x) \in (T \underset{˙}{\oplus} U))$
48	47	ralrimiv	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to \forall x \in (T \underset{˙}{\oplus} U) {inv}_{g} (G) (x) \in (T \underset{˙}{\oplus} U)$
49	3 16	syl	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to G \in Grp$
50	28	issubg3	$⊢ G \in Grp \to (T \underset{˙}{\oplus} U \in SubGrp (G) \leftrightarrow (T \underset{˙}{\oplus} U \in SubMnd (G) \land \forall x \in (T \underset{˙}{\oplus} U) {inv}_{g} (G) (x) \in (T \underset{˙}{\oplus} U)))$
51	49 50	syl	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to (T \underset{˙}{\oplus} U \in SubGrp (G) \leftrightarrow (T \underset{˙}{\oplus} U \in SubMnd (G) \land \forall x \in (T \underset{˙}{\oplus} U) {inv}_{g} (G) (x) \in (T \underset{˙}{\oplus} U)))$
52	11 48 51	mpbir2and	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U \in SubGrp (G)$

Metamath Proof Explorer

Theorem lsmsubg

Proof