Theorem subgdisjb

Description: Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. Analogous to opth , this theorem shows a way of representing a pair of vectors. (Contributed by NM, 5-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$$
Assertion	subgdisjb	$$⊢\phi \to \left(A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\leftrightarrow \left(A=C\wedge B=D\right)\right)$$

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	4	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to T\in \mathrm{SubGrp}\left(G\right)$$
13	5	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to U\in \mathrm{SubGrp}\left(G\right)$$
14	6	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to T\cap U=\left\{\underset{\dot{}}{0}\right\}$$
15	7	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to T\subseteq Z\left(U\right)$$
16	8	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to A\in T$$
17	9	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to C\in T$$
18	10	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to B\in U$$
19	11	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to D\in U$$
20		simpr	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D$$
21	1 2 3 12 13 14 15 16 17 18 19 20	subgdisj1	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to A=C$$
22	1 2 3 12 13 14 15 16 17 18 19 20	subgdisj2	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to B=D$$
23	21 22	jca	$$⊢\left(\phi \wedge A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\right)\to \left(A=C\wedge B=D\right)$$
24	23	ex	$$⊢\phi \to \left(A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\to \left(A=C\wedge B=D\right)\right)$$
25		oveq12	$$⊢\left(A=C\wedge B=D\right)\to A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D$$
26	24 25	impbid1	$$⊢\phi \to \left(A\underset{\dot{}}{+}B=C\underset{\dot{}}{+}D\leftrightarrow \left(A=C\wedge B=D\right)\right)$$