lsmdisj3r

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}$
	lsmdisjr.i	$⊢ φ \to S \cap (T \underset{˙}{\oplus} U) = \{\underset{˙}{0}\}$
	lsmdisj2r.i	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
	lsmdisj3r.z	$⊢ Z = Cntz (G)$
	lsmdisj3r.s	$⊢ φ \to T \subseteq Z (U)$
Assertion	lsmdisj3r	$⊢ φ \to (S \underset{˙}{\oplus} T) \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		lsmdisj2r.i	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
8		lsmdisj3r.z	$⊢ Z = Cntz (G)$
9		lsmdisj3r.s	$⊢ φ \to T \subseteq Z (U)$
10	1 8	lsmcom2	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
11	3 4 9 10	syl3anc	$⊢ φ \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
12	11	ineq2d	$⊢ φ \to S \cap (T \underset{˙}{\oplus} U) = S \cap (U \underset{˙}{\oplus} T)$
13	12 6	eqtr3d	$⊢ φ \to S \cap (U \underset{˙}{\oplus} T) = \{\underset{˙}{0}\}$
14		incom	$⊢ U \cap T = T \cap U$
15	14 7	eqtrid	$⊢ φ \to U \cap T = \{\underset{˙}{0}\}$
16	1 2 4 3 5 13 15	lsmdisj2r	$⊢ φ \to (S \underset{˙}{\oplus} T) \cap U = \{\underset{˙}{0}\}$

Metamath Proof Explorer