This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsmdisj3b

Description: Association of the disjointness constraint in 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}$
		lsmdisj3b.z	$⊢ Z = Cntz (G)$
		lsmdisj3b.2	$⊢ φ \to T \subseteq Z (U)$
	Assertion	lsmdisj3b	$⊢ φ \to (((S \underset{˙}{\oplus} T) \cap U = \{\underset{˙}{0}\} \land S \cap T = \{\underset{˙}{0}\}) \leftrightarrow (S \cap (T \underset{˙}{\oplus} 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		lsmdisj3b.z	$⊢ Z = Cntz (G)$
7		lsmdisj3b.2	$⊢ φ \to T \subseteq Z (U)$
8	1 2 4 3 5	lsmdisj2b	$⊢ φ \to (((S \underset{˙}{\oplus} T) \cap U = \{\underset{˙}{0}\} \land S \cap T = \{\underset{˙}{0}\}) \leftrightarrow (S \cap (U \underset{˙}{\oplus} T) = \{\underset{˙}{0}\} \land U \cap T = \{\underset{˙}{0}\}))$
9	1 6	lsmcom2	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
10	3 4 7 9	syl3anc	$⊢ φ \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
11	10	ineq2d	$⊢ φ \to S \cap (T \underset{˙}{\oplus} U) = S \cap (U \underset{˙}{\oplus} T)$
12	11	eqeq1d	$⊢ φ \to (S \cap (T \underset{˙}{\oplus} U) = \{\underset{˙}{0}\} \leftrightarrow S \cap (U \underset{˙}{\oplus} T) = \{\underset{˙}{0}\})$
13		incom	$⊢ T \cap U = U \cap T$
14	13	a1i	$⊢ φ \to T \cap U = U \cap T$
15	14	eqeq1d	$⊢ φ \to (T \cap U = \{\underset{˙}{0}\} \leftrightarrow U \cap T = \{\underset{˙}{0}\})$
16	12 15	anbi12d	$⊢ φ \to ((S \cap (T \underset{˙}{\oplus} U) = \{\underset{˙}{0}\} \land T \cap U = \{\underset{˙}{0}\}) \leftrightarrow (S \cap (U \underset{˙}{\oplus} T) = \{\underset{˙}{0}\} \land U \cap T = \{\underset{˙}{0}\}))$
17	8 16	bitr4d	$⊢ φ \to (((S \underset{˙}{\oplus} T) \cap U = \{\underset{˙}{0}\} \land S \cap T = \{\underset{˙}{0}\}) \leftrightarrow (S \cap (T \underset{˙}{\oplus} U) = \{\underset{˙}{0}\} \land T \cap U = \{\underset{˙}{0}\}))$