lsmdisj2

Description: Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016)

	Ref	Expression
Hypotheses	lsmcntz.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	lsmcntz.s	$⊢ φ \to S \in SubGrp (G)$
	lsmcntz.t	$⊢ φ \to T \in SubGrp (G)$
	lsmcntz.u	$⊢ φ \to U \in SubGrp (G)$
	lsmdisj.o	$⊢ \underset{˙}{0} = 0_{G}$
	lsmdisj.i	$⊢ φ \to (S \underset{˙}{\oplus} T) \cap U = \{\underset{˙}{0}\}$
	lsmdisj2.i	$⊢ φ \to S \cap T = \{\underset{˙}{0}\}$
Assertion	lsmdisj2	$⊢ φ \to T \cap (S \underset{˙}{\oplus} U) = \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		lsmcntz.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		lsmcntz.s	$⊢ φ \to S \in SubGrp (G)$
3		lsmcntz.t	$⊢ φ \to T \in SubGrp (G)$
4		lsmcntz.u	$⊢ φ \to U \in SubGrp (G)$
5		lsmdisj.o	$⊢ \underset{˙}{0} = 0_{G}$
6		lsmdisj.i	$⊢ φ \to (S \underset{˙}{\oplus} T) \cap U = \{\underset{˙}{0}\}$
7		lsmdisj2.i	$⊢ φ \to S \cap T = \{\underset{˙}{0}\}$
8		eqid	$⊢ +_{G} = +_{G}$
9	8 1	lsmelval	$⊢ (S \in SubGrp (G) \land U \in SubGrp (G)) \to (x \in (S \underset{˙}{\oplus} U) \leftrightarrow \exists s \in S \exists u \in U x = s +_{G} u)$
10	2 4 9	syl2anc	$⊢ φ \to (x \in (S \underset{˙}{\oplus} U) \leftrightarrow \exists s \in S \exists u \in U x = s +_{G} u)$
11		simplrl	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s \in S$
12		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
13	2 12	syl	$⊢ φ \to G \in Grp$
14	13	ad2antrr	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to G \in Grp$
15	2	ad2antrr	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to S \in SubGrp (G)$
16		eqid	$⊢ {Base}_{G} = {Base}_{G}$
17	16	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
18	15 17	syl	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to S \subseteq {Base}_{G}$
19	18 11	sseldd	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s \in {Base}_{G}$
20		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
21	16 8 5 20	grplinv	$⊢ (G \in Grp \land s \in {Base}_{G}) \to {inv}_{g} (G) (s) +_{G} s = \underset{˙}{0}$
22	14 19 21	syl2anc	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to {inv}_{g} (G) (s) +_{G} s = \underset{˙}{0}$
23	22	oveq1d	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to ({inv}_{g} (G) (s) +_{G} s) +_{G} u = \underset{˙}{0} +_{G} u$
24	20	subginvcl	$⊢ (S \in SubGrp (G) \land s \in S) \to {inv}_{g} (G) (s) \in S$
25	15 11 24	syl2anc	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to {inv}_{g} (G) (s) \in S$
26	18 25	sseldd	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to {inv}_{g} (G) (s) \in {Base}_{G}$
27	4	ad2antrr	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to U \in SubGrp (G)$
28	16	subgss	$⊢ U \in SubGrp (G) \to U \subseteq {Base}_{G}$
29	27 28	syl	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to U \subseteq {Base}_{G}$
30		simplrr	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to u \in U$
31	29 30	sseldd	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to u \in {Base}_{G}$
32	16 8	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (s) \in {Base}_{G} \land s \in {Base}_{G} \land u \in {Base}_{G})) \to ({inv}_{g} (G) (s) +_{G} s) +_{G} u = {inv}_{g} (G) (s) +_{G} (s +_{G} u)$
33	14 26 19 31 32	syl13anc	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to ({inv}_{g} (G) (s) +_{G} s) +_{G} u = {inv}_{g} (G) (s) +_{G} (s +_{G} u)$
34	16 8 5	grplid	$⊢ (G \in Grp \land u \in {Base}_{G}) \to \underset{˙}{0} +_{G} u = u$
35	14 31 34	syl2anc	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to \underset{˙}{0} +_{G} u = u$
36	23 33 35	3eqtr3d	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to {inv}_{g} (G) (s) +_{G} (s +_{G} u) = u$
37	3	ad2antrr	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to T \in SubGrp (G)$
38		simpr	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s +_{G} u \in T$
39	8 1	lsmelvali	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G)) \land ({inv}_{g} (G) (s) \in S \land s +_{G} u \in T)) \to {inv}_{g} (G) (s) +_{G} (s +_{G} u) \in (S \underset{˙}{\oplus} T)$
40	15 37 25 38 39	syl22anc	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to {inv}_{g} (G) (s) +_{G} (s +_{G} u) \in (S \underset{˙}{\oplus} T)$
41	36 40	eqeltrrd	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to u \in (S \underset{˙}{\oplus} T)$
42	41 30	elind	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to u \in ((S \underset{˙}{\oplus} T) \cap U)$
43	6	ad2antrr	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to (S \underset{˙}{\oplus} T) \cap U = \{\underset{˙}{0}\}$
44	42 43	eleqtrd	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to u \in \{\underset{˙}{0}\}$
45		elsni	$⊢ u \in \{\underset{˙}{0}\} \to u = \underset{˙}{0}$
46	44 45	syl	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to u = \underset{˙}{0}$
47	46	oveq2d	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s +_{G} u = s +_{G} \underset{˙}{0}$
48	16 8 5	grprid	$⊢ (G \in Grp \land s \in {Base}_{G}) \to s +_{G} \underset{˙}{0} = s$
49	14 19 48	syl2anc	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s +_{G} \underset{˙}{0} = s$
50	47 49	eqtrd	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s +_{G} u = s$
51	50 38	eqeltrrd	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s \in T$
52	11 51	elind	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s \in (S \cap T)$
53	7	ad2antrr	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to S \cap T = \{\underset{˙}{0}\}$
54	52 53	eleqtrd	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s \in \{\underset{˙}{0}\}$
55		elsni	$⊢ s \in \{\underset{˙}{0}\} \to s = \underset{˙}{0}$
56	54 55	syl	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s = \underset{˙}{0}$
57	56 46	oveq12d	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s +_{G} u = \underset{˙}{0} +_{G} \underset{˙}{0}$
58	16 5	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in {Base}_{G}$
59	16 8 5	grplid	$⊢ (G \in Grp \land \underset{˙}{0} \in {Base}_{G}) \to \underset{˙}{0} +_{G} \underset{˙}{0} = \underset{˙}{0}$
60	13 58 59	syl2anc2	$⊢ φ \to \underset{˙}{0} +_{G} \underset{˙}{0} = \underset{˙}{0}$
61	60	ad2antrr	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to \underset{˙}{0} +_{G} \underset{˙}{0} = \underset{˙}{0}$
62	57 61	eqtrd	$⊢ ((φ \land (s \in S \land u \in U)) \land s +_{G} u \in T) \to s +_{G} u = \underset{˙}{0}$
63	62	ex	$⊢ (φ \land (s \in S \land u \in U)) \to (s +_{G} u \in T \to s +_{G} u = \underset{˙}{0})$
64		eleq1	$⊢ x = s +_{G} u \to (x \in T \leftrightarrow s +_{G} u \in T)$
65		eqeq1	$⊢ x = s +_{G} u \to (x = \underset{˙}{0} \leftrightarrow s +_{G} u = \underset{˙}{0})$
66	64 65	imbi12d	$⊢ x = s +_{G} u \to ((x \in T \to x = \underset{˙}{0}) \leftrightarrow (s +_{G} u \in T \to s +_{G} u = \underset{˙}{0}))$
67	63 66	syl5ibrcom	$⊢ (φ \land (s \in S \land u \in U)) \to (x = s +_{G} u \to (x \in T \to x = \underset{˙}{0}))$
68	67	rexlimdvva	$⊢ φ \to (\exists s \in S \exists u \in U x = s +_{G} u \to (x \in T \to x = \underset{˙}{0}))$
69	10 68	sylbid	$⊢ φ \to (x \in (S \underset{˙}{\oplus} U) \to (x \in T \to x = \underset{˙}{0}))$
70	69	impcomd	$⊢ φ \to ((x \in T \land x \in (S \underset{˙}{\oplus} U)) \to x = \underset{˙}{0})$
71		elin	$⊢ x \in (T \cap (S \underset{˙}{\oplus} U)) \leftrightarrow (x \in T \land x \in (S \underset{˙}{\oplus} U))$
72		velsn	$⊢ x \in \{\underset{˙}{0}\} \leftrightarrow x = \underset{˙}{0}$
73	70 71 72	3imtr4g	$⊢ φ \to (x \in (T \cap (S \underset{˙}{\oplus} U)) \to x \in \{\underset{˙}{0}\})$
74	73	ssrdv	$⊢ φ \to T \cap (S \underset{˙}{\oplus} U) \subseteq \{\underset{˙}{0}\}$
75	5	subg0cl	$⊢ T \in SubGrp (G) \to \underset{˙}{0} \in T$
76	3 75	syl	$⊢ φ \to \underset{˙}{0} \in T$
77	1	lsmub1	$⊢ (S \in SubGrp (G) \land U \in SubGrp (G)) \to S \subseteq S \underset{˙}{\oplus} U$
78	2 4 77	syl2anc	$⊢ φ \to S \subseteq S \underset{˙}{\oplus} U$
79	5	subg0cl	$⊢ S \in SubGrp (G) \to \underset{˙}{0} \in S$
80	2 79	syl	$⊢ φ \to \underset{˙}{0} \in S$
81	78 80	sseldd	$⊢ φ \to \underset{˙}{0} \in (S \underset{˙}{\oplus} U)$
82	76 81	elind	$⊢ φ \to \underset{˙}{0} \in (T \cap (S \underset{˙}{\oplus} U))$
83	82	snssd	$⊢ φ \to \{\underset{˙}{0}\} \subseteq T \cap (S \underset{˙}{\oplus} U)$
84	74 83	eqssd	$⊢ φ \to T \cap (S \underset{˙}{\oplus} U) = \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem lsmdisj2

Proof