lsmdisjr

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}$
	lsmdisjr.i	$⊢ φ \to S \cap (T \underset{˙}{\oplus} U) = \{\underset{˙}{0}\}$
Assertion	lsmdisjr	$⊢ φ \to (S \cap T = \{\underset{˙}{0}\} \land S \cap U = \{\underset{˙}{0}\})$

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		lsmdisjr.i	$⊢ φ \to S \cap (T \underset{˙}{\oplus} U) = \{\underset{˙}{0}\}$
7		incom	$⊢ S \cap (T \underset{˙}{\oplus} U) = (T \underset{˙}{\oplus} U) \cap S$
8	7 6	eqtr3id	$⊢ φ \to (T \underset{˙}{\oplus} U) \cap S = \{\underset{˙}{0}\}$
9	1 3 4 2 5 8	lsmdisj	$⊢ φ \to (T \cap S = \{\underset{˙}{0}\} \land U \cap S = \{\underset{˙}{0}\})$
10		incom	$⊢ T \cap S = S \cap T$
11	10	eqeq1i	$⊢ T \cap S = \{\underset{˙}{0}\} \leftrightarrow S \cap T = \{\underset{˙}{0}\}$
12		incom	$⊢ U \cap S = S \cap U$
13	12	eqeq1i	$⊢ U \cap S = \{\underset{˙}{0}\} \leftrightarrow S \cap U = \{\underset{˙}{0}\}$
14	11 13	anbi12i	$⊢ (T \cap S = \{\underset{˙}{0}\} \land U \cap S = \{\underset{˙}{0}\}) \leftrightarrow (S \cap T = \{\underset{˙}{0}\} \land S \cap U = \{\underset{˙}{0}\})$
15	9 14	sylib	$⊢ φ \to (S \cap T = \{\underset{˙}{0}\} \land S \cap U = \{\underset{˙}{0}\})$

Metamath Proof Explorer