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

Metamath Proof Explorer

Theorem lsmdisj3a

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)$
		lsmdisj3a.2	$⊢ φ \to S \subseteq Z (T)$
	Assertion	lsmdisj3a	$⊢ φ \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		lsmdisj3a.2	$⊢ φ \to S \subseteq Z (T)$
8	1 6	lsmcom2	$⊢ (S \in SubGrp (G) \land T \in SubGrp (G) \land S \subseteq Z (T)) \to S \underset{˙}{\oplus} T = T \underset{˙}{\oplus} S$
9	2 3 7 8	syl3anc	$⊢ φ \to S \underset{˙}{\oplus} T = T \underset{˙}{\oplus} S$
10	9	ineq1d	$⊢ φ \to (S \underset{˙}{\oplus} T) \cap U = (T \underset{˙}{\oplus} S) \cap U$
11	10	eqeq1d	$⊢ φ \to ((S \underset{˙}{\oplus} T) \cap U = \{\underset{˙}{0}\} \leftrightarrow (T \underset{˙}{\oplus} S) \cap U = \{\underset{˙}{0}\})$
12		incom	$⊢ S \cap T = T \cap S$
13	12	a1i	$⊢ φ \to S \cap T = T \cap S$
14	13	eqeq1d	$⊢ φ \to (S \cap T = \{\underset{˙}{0}\} \leftrightarrow T \cap S = \{\underset{˙}{0}\})$
15	11 14	anbi12d	$⊢ φ \to (((S \underset{˙}{\oplus} T) \cap U = \{\underset{˙}{0}\} \land S \cap T = \{\underset{˙}{0}\}) \leftrightarrow ((T \underset{˙}{\oplus} S) \cap U = \{\underset{˙}{0}\} \land T \cap S = \{\underset{˙}{0}\}))$
16	1 3 2 4 5	lsmdisj2a	$⊢ φ \to (((T \underset{˙}{\oplus} S) \cap U = \{\underset{˙}{0}\} \land T \cap S = \{\underset{˙}{0}\}) \leftrightarrow (S \cap (T \underset{˙}{\oplus} U) = \{\underset{˙}{0}\} \land T \cap U = \{\underset{˙}{0}\}))$
17	15 16	bitrd	$⊢ φ \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}\}))$