lsmsubm

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

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

Proof

Step	Hyp	Ref	Expression
1		lsmsubg.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		lsmsubg.z	$⊢ Z = Cntz (G)$
3		submrcl	$⊢ T \in SubMnd (G) \to G \in Mnd$
4	3	3ad2ant1	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to G \in Mnd$
5		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6	5	submss	$⊢ T \in SubMnd (G) \to T \subseteq {Base}_{G}$
7	6	3ad2ant1	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to T \subseteq {Base}_{G}$
8	5	submss	$⊢ U \in SubMnd (G) \to U \subseteq {Base}_{G}$
9	8	3ad2ant2	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to U \subseteq {Base}_{G}$
10	5 1	lsmssv	$⊢ (G \in Mnd \land T \subseteq {Base}_{G} \land U \subseteq {Base}_{G}) \to T \underset{˙}{\oplus} U \subseteq {Base}_{G}$
11	4 7 9 10	syl3anc	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U \subseteq {Base}_{G}$
12		simp2	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to U \in SubMnd (G)$
13	5 1	lsmub1x	$⊢ (T \subseteq {Base}_{G} \land U \in SubMnd (G)) \to T \subseteq T \underset{˙}{\oplus} U$
14	7 12 13	syl2anc	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to T \subseteq T \underset{˙}{\oplus} U$
15		eqid	$⊢ 0_{G} = 0_{G}$
16	15	subm0cl	$⊢ T \in SubMnd (G) \to 0_{G} \in T$
17	16	3ad2ant1	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to 0_{G} \in T$
18	14 17	sseldd	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to 0_{G} \in (T \underset{˙}{\oplus} U)$
19		eqid	$⊢ +_{G} = +_{G}$
20	5 19 1	lsmelvalx	$⊢ (G \in Mnd \land T \subseteq {Base}_{G} \land U \subseteq {Base}_{G}) \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists a \in T \exists c \in U x = a +_{G} c)$
21	4 7 9 20	syl3anc	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists a \in T \exists c \in U x = a +_{G} c)$
22	5 19 1	lsmelvalx	$⊢ (G \in Mnd \land T \subseteq {Base}_{G} \land U \subseteq {Base}_{G}) \to (y \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists b \in T \exists d \in U y = b +_{G} d)$
23	4 7 9 22	syl3anc	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to (y \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists b \in T \exists d \in U y = b +_{G} d)$
24	21 23	anbi12d	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to ((x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U)) \leftrightarrow (\exists a \in T \exists c \in U x = a +_{G} c \land \exists b \in T \exists d \in U y = b +_{G} d))$
25		reeanv	$⊢ \exists a \in T \exists b \in T (\exists c \in U x = a +_{G} c \land \exists d \in U y = b +_{G} d) \leftrightarrow (\exists a \in T \exists c \in U x = a +_{G} c \land \exists b \in T \exists d \in U y = b +_{G} d)$
26		reeanv	$⊢ \exists c \in U \exists d \in U (x = a +_{G} c \land y = b +_{G} d) \leftrightarrow (\exists c \in U x = a +_{G} c \land \exists d \in U y = b +_{G} d)$
27	4	adantr	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to G \in Mnd$
28	7	adantr	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to T \subseteq {Base}_{G}$
29		simprll	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to a \in T$
30	28 29	sseldd	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to a \in {Base}_{G}$
31		simprlr	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to b \in T$
32	28 31	sseldd	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to b \in {Base}_{G}$
33	9	adantr	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to U \subseteq {Base}_{G}$
34		simprrl	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to c \in U$
35	33 34	sseldd	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to c \in {Base}_{G}$
36		simprrr	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to d \in U$
37	33 36	sseldd	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to d \in {Base}_{G}$
38		simpl3	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to T \subseteq Z (U)$
39	38 31	sseldd	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to b \in Z (U)$
40	19 2	cntzi	$⊢ (b \in Z (U) \land c \in U) \to b +_{G} c = c +_{G} b$
41	39 34 40	syl2anc	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to b +_{G} c = c +_{G} b$
42	5 19 27 30 32 35 37 41	mnd4g	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to (a +_{G} b) +_{G} (c +_{G} d) = (a +_{G} c) +_{G} (b +_{G} d)$
43		simpl1	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to T \in SubMnd (G)$
44	19	submcl	$⊢ (T \in SubMnd (G) \land a \in T \land b \in T) \to a +_{G} b \in T$
45	43 29 31 44	syl3anc	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to a +_{G} b \in T$
46		simpl2	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to U \in SubMnd (G)$
47	19	submcl	$⊢ (U \in SubMnd (G) \land c \in U \land d \in U) \to c +_{G} d \in U$
48	46 34 36 47	syl3anc	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to c +_{G} d \in U$
49	5 19 1	lsmelvalix	$⊢ ((G \in Mnd \land T \subseteq {Base}_{G} \land U \subseteq {Base}_{G}) \land (a +_{G} b \in T \land c +_{G} d \in U)) \to (a +_{G} b) +_{G} (c +_{G} d) \in (T \underset{˙}{\oplus} U)$
50	27 28 33 45 48 49	syl32anc	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to (a +_{G} b) +_{G} (c +_{G} d) \in (T \underset{˙}{\oplus} U)$
51	42 50	eqeltrrd	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to (a +_{G} c) +_{G} (b +_{G} d) \in (T \underset{˙}{\oplus} U)$
52		oveq12	$⊢ (x = a +_{G} c \land y = b +_{G} d) \to x +_{G} y = (a +_{G} c) +_{G} (b +_{G} d)$
53	52	eleq1d	$⊢ (x = a +_{G} c \land y = b +_{G} d) \to (x +_{G} y \in (T \underset{˙}{\oplus} U) \leftrightarrow (a +_{G} c) +_{G} (b +_{G} d) \in (T \underset{˙}{\oplus} U))$
54	51 53	syl5ibrcom	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land ((a \in T \land b \in T) \land (c \in U \land d \in U))) \to ((x = a +_{G} c \land y = b +_{G} d) \to x +_{G} y \in (T \underset{˙}{\oplus} U))$
55	54	anassrs	$⊢ (((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land (a \in T \land b \in T)) \land (c \in U \land d \in U)) \to ((x = a +_{G} c \land y = b +_{G} d) \to x +_{G} y \in (T \underset{˙}{\oplus} U))$
56	55	rexlimdvva	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land (a \in T \land b \in T)) \to (\exists c \in U \exists d \in U (x = a +_{G} c \land y = b +_{G} d) \to x +_{G} y \in (T \underset{˙}{\oplus} U))$
57	26 56	biimtrrid	$⊢ ((T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \land (a \in T \land b \in T)) \to ((\exists c \in U x = a +_{G} c \land \exists d \in U y = b +_{G} d) \to x +_{G} y \in (T \underset{˙}{\oplus} U))$
58	57	rexlimdvva	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to (\exists a \in T \exists b \in T (\exists c \in U x = a +_{G} c \land \exists d \in U y = b +_{G} d) \to x +_{G} y \in (T \underset{˙}{\oplus} U))$
59	25 58	biimtrrid	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to ((\exists a \in T \exists c \in U x = a +_{G} c \land \exists b \in T \exists d \in U y = b +_{G} d) \to x +_{G} y \in (T \underset{˙}{\oplus} U))$
60	24 59	sylbid	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to ((x \in (T \underset{˙}{\oplus} U) \land y \in (T \underset{˙}{\oplus} U)) \to x +_{G} y \in (T \underset{˙}{\oplus} U))$
61	60	ralrimivv	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to \forall x \in (T \underset{˙}{\oplus} U) \forall y \in (T \underset{˙}{\oplus} U) x +_{G} y \in (T \underset{˙}{\oplus} U)$
62	5 15 19	issubm	$⊢ G \in Mnd \to (T \underset{˙}{\oplus} U \in SubMnd (G) \leftrightarrow (T \underset{˙}{\oplus} U \subseteq {Base}_{G} \land 0_{G} \in (T \underset{˙}{\oplus} U) \land \forall x \in (T \underset{˙}{\oplus} U) \forall y \in (T \underset{˙}{\oplus} U) x +_{G} y \in (T \underset{˙}{\oplus} U)))$
63	4 62	syl	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to (T \underset{˙}{\oplus} U \in SubMnd (G) \leftrightarrow (T \underset{˙}{\oplus} U \subseteq {Base}_{G} \land 0_{G} \in (T \underset{˙}{\oplus} U) \land \forall x \in (T \underset{˙}{\oplus} U) \forall y \in (T \underset{˙}{\oplus} U) x +_{G} y \in (T \underset{˙}{\oplus} U)))$
64	11 18 61 63	mpbir3and	$⊢ (T \in SubMnd (G) \land U \in SubMnd (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U \in SubMnd (G)$

Metamath Proof Explorer

Theorem lsmsubm

Proof