lsmdisj

Description: Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-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}\}$
Assertion	lsmdisj	$⊢ φ \to (S \cap U = \{\underset{˙}{0}\} \land T \cap 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	1	lsmub1	$⊢ (S \in SubGrp (G) \land T \in SubGrp (G)) \to S \subseteq S \underset{˙}{\oplus} T$
8	2 3 7	syl2anc	$⊢ φ \to S \subseteq S \underset{˙}{\oplus} T$
9	8	ssrind	$⊢ φ \to S \cap U \subseteq (S \underset{˙}{\oplus} T) \cap U$
10	9 6	sseqtrd	$⊢ φ \to S \cap U \subseteq \{\underset{˙}{0}\}$
11	5	subg0cl	$⊢ S \in SubGrp (G) \to \underset{˙}{0} \in S$
12	2 11	syl	$⊢ φ \to \underset{˙}{0} \in S$
13	5	subg0cl	$⊢ U \in SubGrp (G) \to \underset{˙}{0} \in U$
14	4 13	syl	$⊢ φ \to \underset{˙}{0} \in U$
15	12 14	elind	$⊢ φ \to \underset{˙}{0} \in (S \cap U)$
16	15	snssd	$⊢ φ \to \{\underset{˙}{0}\} \subseteq S \cap U$
17	10 16	eqssd	$⊢ φ \to S \cap U = \{\underset{˙}{0}\}$
18	1	lsmub2	$⊢ (S \in SubGrp (G) \land T \in SubGrp (G)) \to T \subseteq S \underset{˙}{\oplus} T$
19	2 3 18	syl2anc	$⊢ φ \to T \subseteq S \underset{˙}{\oplus} T$
20	19	ssrind	$⊢ φ \to T \cap U \subseteq (S \underset{˙}{\oplus} T) \cap U$
21	20 6	sseqtrd	$⊢ φ \to T \cap U \subseteq \{\underset{˙}{0}\}$
22	5	subg0cl	$⊢ T \in SubGrp (G) \to \underset{˙}{0} \in T$
23	3 22	syl	$⊢ φ \to \underset{˙}{0} \in T$
24	23 14	elind	$⊢ φ \to \underset{˙}{0} \in (T \cap U)$
25	24	snssd	$⊢ φ \to \{\underset{˙}{0}\} \subseteq T \cap U$
26	21 25	eqssd	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
27	17 26	jca	$⊢ φ \to (S \cap U = \{\underset{˙}{0}\} \land T \cap U = \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem lsmdisj

Proof