subgdisj2

Description: Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. (Contributed by NM, 12-Jul-2014) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	subgdisj.p	$⊢ \underset{˙}{+} = +_{G}$
	subgdisj.o	$⊢ \underset{˙}{0} = 0_{G}$
	subgdisj.z	$⊢ Z = Cntz (G)$
	subgdisj.t	$⊢ φ \to T \in SubGrp (G)$
	subgdisj.u	$⊢ φ \to U \in SubGrp (G)$
	subgdisj.i	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
	subgdisj.s	$⊢ φ \to T \subseteq Z (U)$
	subgdisj.a	$⊢ φ \to A \in T$
	subgdisj.c	$⊢ φ \to C \in T$
	subgdisj.b	$⊢ φ \to B \in U$
	subgdisj.d	$⊢ φ \to D \in U$
	subgdisj.j	$⊢ φ \to A \underset{˙}{+} B = C \underset{˙}{+} D$
Assertion	subgdisj2	$⊢ φ \to B = D$

Proof

Step	Hyp	Ref	Expression
1		subgdisj.p	$⊢ \underset{˙}{+} = +_{G}$
2		subgdisj.o	$⊢ \underset{˙}{0} = 0_{G}$
3		subgdisj.z	$⊢ Z = Cntz (G)$
4		subgdisj.t	$⊢ φ \to T \in SubGrp (G)$
5		subgdisj.u	$⊢ φ \to U \in SubGrp (G)$
6		subgdisj.i	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
7		subgdisj.s	$⊢ φ \to T \subseteq Z (U)$
8		subgdisj.a	$⊢ φ \to A \in T$
9		subgdisj.c	$⊢ φ \to C \in T$
10		subgdisj.b	$⊢ φ \to B \in U$
11		subgdisj.d	$⊢ φ \to D \in U$
12		subgdisj.j	$⊢ φ \to A \underset{˙}{+} B = C \underset{˙}{+} D$
13		incom	$⊢ T \cap U = U \cap T$
14	13 6	eqtr3id	$⊢ φ \to U \cap T = \{\underset{˙}{0}\}$
15	3 4 5 7	cntzrecd	$⊢ φ \to U \subseteq Z (T)$
16	7 8	sseldd	$⊢ φ \to A \in Z (U)$
17	1 3	cntzi	$⊢ (A \in Z (U) \land B \in U) \to A \underset{˙}{+} B = B \underset{˙}{+} A$
18	16 10 17	syl2anc	$⊢ φ \to A \underset{˙}{+} B = B \underset{˙}{+} A$
19	7 9	sseldd	$⊢ φ \to C \in Z (U)$
20	1 3	cntzi	$⊢ (C \in Z (U) \land D \in U) \to C \underset{˙}{+} D = D \underset{˙}{+} C$
21	19 11 20	syl2anc	$⊢ φ \to C \underset{˙}{+} D = D \underset{˙}{+} C$
22	12 18 21	3eqtr3d	$⊢ φ \to B \underset{˙}{+} A = D \underset{˙}{+} C$
23	1 2 3 5 4 14 15 10 11 8 9 22	subgdisj1	$⊢ φ \to B = D$

Metamath Proof Explorer

Theorem subgdisj2

Proof