lsmmod

Description: The modular law holds for subgroup sum. Similar to part of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2016)

		Ref	Expression
	Hypothesis	lsmmod.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	Assertion	lsmmod	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to S \underset{˙}{\oplus} (T \cap U) = (S \underset{˙}{\oplus} T) \cap U$

Proof

Step	Hyp	Ref	Expression
1		lsmmod.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		simpl1	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to S \in SubGrp (G)$
3		simpl2	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to T \in SubGrp (G)$
4		inss1	$⊢ T \cap U \subseteq T$
5	4	a1i	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to T \cap U \subseteq T$
6	1	lsmless2	$⊢ (S \in SubGrp (G) \land T \in SubGrp (G) \land T \cap U \subseteq T) \to S \underset{˙}{\oplus} (T \cap U) \subseteq S \underset{˙}{\oplus} T$
7	2 3 5 6	syl3anc	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to S \underset{˙}{\oplus} (T \cap U) \subseteq S \underset{˙}{\oplus} T$
8		simpr	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to S \subseteq U$
9		inss2	$⊢ T \cap U \subseteq U$
10	9	a1i	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to T \cap U \subseteq U$
11		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
12		eqid	$⊢ {Base}_{G} = {Base}_{G}$
13	12	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
14		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
15	2 11 13 14	4syl	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to SubGrp (G) \in Moore ({Base}_{G})$
16		simpl3	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to U \in SubGrp (G)$
17		mreincl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to T \cap U \in SubGrp (G)$
18	15 3 16 17	syl3anc	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to T \cap U \in SubGrp (G)$
19	1	lsmlub	$⊢ (S \in SubGrp (G) \land T \cap U \in SubGrp (G) \land U \in SubGrp (G)) \to ((S \subseteq U \land T \cap U \subseteq U) \leftrightarrow S \underset{˙}{\oplus} (T \cap U) \subseteq U)$
20	2 18 16 19	syl3anc	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to ((S \subseteq U \land T \cap U \subseteq U) \leftrightarrow S \underset{˙}{\oplus} (T \cap U) \subseteq U)$
21	8 10 20	mpbi2and	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to S \underset{˙}{\oplus} (T \cap U) \subseteq U$
22	7 21	ssind	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to S \underset{˙}{\oplus} (T \cap U) \subseteq (S \underset{˙}{\oplus} T) \cap U$
23		elin	$⊢ x \in ((S \underset{˙}{\oplus} T) \cap U) \leftrightarrow (x \in (S \underset{˙}{\oplus} T) \land x \in U)$
24		eqid	$⊢ +_{G} = +_{G}$
25	24 1	lsmelval	$⊢ (S \in SubGrp (G) \land T \in SubGrp (G)) \to (x \in (S \underset{˙}{\oplus} T) \leftrightarrow \exists y \in S \exists z \in T x = y +_{G} z)$
26	2 3 25	syl2anc	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to (x \in (S \underset{˙}{\oplus} T) \leftrightarrow \exists y \in S \exists z \in T x = y +_{G} z)$
27	2	adantr	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to S \in SubGrp (G)$
28	18	adantr	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to T \cap U \in SubGrp (G)$
29		simprll	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to y \in S$
30		simprlr	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to z \in T$
31	27 11	syl	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to G \in Grp$
32	16	adantr	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to U \in SubGrp (G)$
33	12	subgss	$⊢ U \in SubGrp (G) \to U \subseteq {Base}_{G}$
34	32 33	syl	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to U \subseteq {Base}_{G}$
35	8	adantr	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to S \subseteq U$
36	35 29	sseldd	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to y \in U$
37	34 36	sseldd	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to y \in {Base}_{G}$
38		eqid	$⊢ 0_{G} = 0_{G}$
39		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
40	12 24 38 39	grplinv	$⊢ (G \in Grp \land y \in {Base}_{G}) \to {inv}_{g} (G) (y) +_{G} y = 0_{G}$
41	31 37 40	syl2anc	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to {inv}_{g} (G) (y) +_{G} y = 0_{G}$
42	41	oveq1d	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to ({inv}_{g} (G) (y) +_{G} y) +_{G} z = 0_{G} +_{G} z$
43	39	subginvcl	$⊢ (U \in SubGrp (G) \land y \in U) \to {inv}_{g} (G) (y) \in U$
44	32 36 43	syl2anc	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to {inv}_{g} (G) (y) \in U$
45	34 44	sseldd	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to {inv}_{g} (G) (y) \in {Base}_{G}$
46		simpll2	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to T \in SubGrp (G)$
47	12	subgss	$⊢ T \in SubGrp (G) \to T \subseteq {Base}_{G}$
48	46 47	syl	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to T \subseteq {Base}_{G}$
49	48 30	sseldd	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to z \in {Base}_{G}$
50	12 24	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (y) \in {Base}_{G} \land y \in {Base}_{G} \land z \in {Base}_{G})) \to ({inv}_{g} (G) (y) +_{G} y) +_{G} z = {inv}_{g} (G) (y) +_{G} (y +_{G} z)$
51	31 45 37 49 50	syl13anc	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to ({inv}_{g} (G) (y) +_{G} y) +_{G} z = {inv}_{g} (G) (y) +_{G} (y +_{G} z)$
52	12 24 38	grplid	$⊢ (G \in Grp \land z \in {Base}_{G}) \to 0_{G} +_{G} z = z$
53	31 49 52	syl2anc	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to 0_{G} +_{G} z = z$
54	42 51 53	3eqtr3d	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to {inv}_{g} (G) (y) +_{G} (y +_{G} z) = z$
55		simprr	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to y +_{G} z \in U$
56	24	subgcl	$⊢ (U \in SubGrp (G) \land {inv}_{g} (G) (y) \in U \land y +_{G} z \in U) \to {inv}_{g} (G) (y) +_{G} (y +_{G} z) \in U$
57	32 44 55 56	syl3anc	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to {inv}_{g} (G) (y) +_{G} (y +_{G} z) \in U$
58	54 57	eqeltrrd	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to z \in U$
59	30 58	elind	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to z \in (T \cap U)$
60	24 1	lsmelvali	$⊢ ((S \in SubGrp (G) \land T \cap U \in SubGrp (G)) \land (y \in S \land z \in (T \cap U))) \to y +_{G} z \in (S \underset{˙}{\oplus} (T \cap U))$
61	27 28 29 59 60	syl22anc	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land ((y \in S \land z \in T) \land y +_{G} z \in U)) \to y +_{G} z \in (S \underset{˙}{\oplus} (T \cap U))$
62	61	expr	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land (y \in S \land z \in T)) \to (y +_{G} z \in U \to y +_{G} z \in (S \underset{˙}{\oplus} (T \cap U)))$
63		eleq1	$⊢ x = y +_{G} z \to (x \in U \leftrightarrow y +_{G} z \in U)$
64		eleq1	$⊢ x = y +_{G} z \to (x \in (S \underset{˙}{\oplus} (T \cap U)) \leftrightarrow y +_{G} z \in (S \underset{˙}{\oplus} (T \cap U)))$
65	63 64	imbi12d	$⊢ x = y +_{G} z \to ((x \in U \to x \in (S \underset{˙}{\oplus} (T \cap U))) \leftrightarrow (y +_{G} z \in U \to y +_{G} z \in (S \underset{˙}{\oplus} (T \cap U))))$
66	62 65	syl5ibrcom	$⊢ (((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \land (y \in S \land z \in T)) \to (x = y +_{G} z \to (x \in U \to x \in (S \underset{˙}{\oplus} (T \cap U))))$
67	66	rexlimdvva	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to (\exists y \in S \exists z \in T x = y +_{G} z \to (x \in U \to x \in (S \underset{˙}{\oplus} (T \cap U))))$
68	26 67	sylbid	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to (x \in (S \underset{˙}{\oplus} T) \to (x \in U \to x \in (S \underset{˙}{\oplus} (T \cap U))))$
69	68	impd	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to ((x \in (S \underset{˙}{\oplus} T) \land x \in U) \to x \in (S \underset{˙}{\oplus} (T \cap U)))$
70	23 69	syl5bi	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to (x \in ((S \underset{˙}{\oplus} T) \cap U) \to x \in (S \underset{˙}{\oplus} (T \cap U)))$
71	70	ssrdv	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to (S \underset{˙}{\oplus} T) \cap U \subseteq S \underset{˙}{\oplus} (T \cap U)$
72	22 71	eqssd	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land S \subseteq U) \to S \underset{˙}{\oplus} (T \cap U) = (S \underset{˙}{\oplus} T) \cap U$

Metamath Proof Explorer

Theorem lsmmod

Proof