Theorem 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{\dot{}}{+}={+}_G$$
	subgdisj.o	$$⊢\underset{\dot{}}{0}=0_G$$
	subgdisj.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	subgdisj.t	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
	subgdisj.u	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
	subgdisj.i	$$⊢\phi \to T\cap U=\left\{\underset{\dot{}}{0}\right\}$$
	subgdisj.s	$$⊢\phi \to T\subseteq Z\left(U\right)$$
	subgdisj.a	$$⊢\phi \to A\in T$$
	subgdisj.c	$$⊢\phi \to C\in T$$
	subgdisj.b	$$⊢\phi \to B\in U$$
	subgdisj.d	$$⊢\phi \to D\in U$$
	subgdisj.j	$$⊢\phi \to A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D$$
Assertion	subgdisj2	$$⊢\phi \to B=D$$

Proof

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