Theorem subgdisj1

Description: Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. (Contributed by NM, 2-Apr-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	subgdisj1	$$⊢\phi \to A=C$$

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		eqid	$$⊢{-}_G={-}_G$$
14	13	subgsubcl	$$⊢\left(T\in \mathrm{SubGrp}\left(G\right)\wedge A\in T\wedge C\in T\right)\to A{-}_{G}C\in T$$
15	4 8 9 14	syl3anc	$$⊢\phi \to A{-}_{G}C\in T$$
16	7 9	sseldd	$$⊢\phi \to C\in Z\left(U\right)$$
17	1 3	cntzi	$$⊢\left(C\in Z\left(U\right)\wedge B\in U\right)\to C\underset{\dot{}}{+}B=B\underset{\dot{}}{+}C$$
18	16 10 17	syl2anc	$$⊢\phi \to C\underset{\dot{}}{+}B=B\underset{\dot{}}{+}C$$
19	12 18	oveq12d	$$⊢\phi \to \left(A\underset{\dot{}}{+}B\right){-}_G\left(C\underset{\dot{}}{+}B\right)=\left(C\underset{\dot{}}{+}D\right){-}_G\left(B\underset{\dot{}}{+}C\right)$$
20		subgrcl	$$⊢T\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$
21	4 20	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
22		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
23	22	subgss	$$⊢T\in \mathrm{SubGrp}\left(G\right)\to T\subseteq {\mathrm{Base}}_G$$
24	4 23	syl	$$⊢\phi \to T\subseteq {\mathrm{Base}}_G$$
25	24 8	sseldd	$$⊢\phi \to A\in {\mathrm{Base}}_G$$
26	22	subgss	$$⊢U\in \mathrm{SubGrp}\left(G\right)\to U\subseteq {\mathrm{Base}}_G$$
27	5 26	syl	$$⊢\phi \to U\subseteq {\mathrm{Base}}_G$$
28	27 10	sseldd	$$⊢\phi \to B\in {\mathrm{Base}}_G$$
29	22 1	grpcl	$$⊢\left(G\in \mathrm{Grp}\wedge A\in {\mathrm{Base}}_G\wedge B\in {\mathrm{Base}}_G\right)\to A\underset{\dot{}}{+}B\in {\mathrm{Base}}_G$$
30	21 25 28 29	syl3anc	$$⊢\phi \to A\underset{\dot{}}{+}B\in {\mathrm{Base}}_G$$
31	24 9	sseldd	$$⊢\phi \to C\in {\mathrm{Base}}_G$$
32	22 1 13	grpsubsub4	$$⊢\left(G\in \mathrm{Grp}\wedge \left(A\underset{\dot{}}{+}B\in {\mathrm{Base}}_G\wedge B\in {\mathrm{Base}}_G\wedge C\in {\mathrm{Base}}_G\right)\right)\to \left(\left(A\underset{\dot{}}{+}B\right){-}_{G}B\right){-}_{G}C=\left(A\underset{\dot{}}{+}B\right){-}_G\left(C\underset{\dot{}}{+}B\right)$$
33	21 30 28 31 32	syl13anc	$$⊢\phi \to \left(\left(A\underset{\dot{}}{+}B\right){-}_{G}B\right){-}_{G}C=\left(A\underset{\dot{}}{+}B\right){-}_G\left(C\underset{\dot{}}{+}B\right)$$
34	12 30	eqeltrrd	$$⊢\phi \to C\underset{\dot{}}{+}D\in {\mathrm{Base}}_G$$
35	22 1 13	grpsubsub4	$$⊢\left(G\in \mathrm{Grp}\wedge \left(C\underset{\dot{}}{+}D\in {\mathrm{Base}}_G\wedge C\in {\mathrm{Base}}_G\wedge B\in {\mathrm{Base}}_G\right)\right)\to \left(\left(C\underset{\dot{}}{+}D\right){-}_{G}C\right){-}_{G}B=\left(C\underset{\dot{}}{+}D\right){-}_G\left(B\underset{\dot{}}{+}C\right)$$
36	21 34 31 28 35	syl13anc	$$⊢\phi \to \left(\left(C\underset{\dot{}}{+}D\right){-}_{G}C\right){-}_{G}B=\left(C\underset{\dot{}}{+}D\right){-}_G\left(B\underset{\dot{}}{+}C\right)$$
37	19 33 36	3eqtr4d	$$⊢\phi \to \left(\left(A\underset{\dot{}}{+}B\right){-}_{G}B\right){-}_{G}C=\left(\left(C\underset{\dot{}}{+}D\right){-}_{G}C\right){-}_{G}B$$
38	22 1 13	grppncan	$$⊢\left(G\in \mathrm{Grp}\wedge A\in {\mathrm{Base}}_G\wedge B\in {\mathrm{Base}}_G\right)\to \left(A\underset{\dot{}}{+}B\right){-}_{G}B=A$$
39	21 25 28 38	syl3anc	$$⊢\phi \to \left(A\underset{\dot{}}{+}B\right){-}_{G}B=A$$
40	39	oveq1d	$$⊢\phi \to \left(\left(A\underset{\dot{}}{+}B\right){-}_{G}B\right){-}_{G}C=A{-}_{G}C$$
41	1 3	cntzi	$$⊢\left(C\in Z\left(U\right)\wedge D\in U\right)\to C\underset{\dot{}}{+}D=D\underset{\dot{}}{+}C$$
42	16 11 41	syl2anc	$$⊢\phi \to C\underset{\dot{}}{+}D=D\underset{\dot{}}{+}C$$
43	42	oveq1d	$$⊢\phi \to \left(C\underset{\dot{}}{+}D\right){-}_{G}C=\left(D\underset{\dot{}}{+}C\right){-}_{G}C$$
44	27 11	sseldd	$$⊢\phi \to D\in {\mathrm{Base}}_G$$
45	22 1 13	grppncan	$$⊢\left(G\in \mathrm{Grp}\wedge D\in {\mathrm{Base}}_G\wedge C\in {\mathrm{Base}}_G\right)\to \left(D\underset{\dot{}}{+}C\right){-}_{G}C=D$$
46	21 44 31 45	syl3anc	$$⊢\phi \to \left(D\underset{\dot{}}{+}C\right){-}_{G}C=D$$
47	43 46	eqtrd	$$⊢\phi \to \left(C\underset{\dot{}}{+}D\right){-}_{G}C=D$$
48	47	oveq1d	$$⊢\phi \to \left(\left(C\underset{\dot{}}{+}D\right){-}_{G}C\right){-}_{G}B=D{-}_{G}B$$
49	37 40 48	3eqtr3d	$$⊢\phi \to A{-}_{G}C=D{-}_{G}B$$
50	13	subgsubcl	$$⊢\left(U\in \mathrm{SubGrp}\left(G\right)\wedge D\in U\wedge B\in U\right)\to D{-}_{G}B\in U$$
51	5 11 10 50	syl3anc	$$⊢\phi \to D{-}_{G}B\in U$$
52	49 51	eqeltrd	$$⊢\phi \to A{-}_{G}C\in U$$
53	15 52	elind	$$⊢\phi \to A{-}_{G}C\in \left(T\cap U\right)$$
54	53 6	eleqtrd	$$⊢\phi \to A{-}_{G}C\in \left\{\underset{\dot{}}{0}\right\}$$
55		elsni	$$⊢A{-}_{G}C\in \left\{\underset{\dot{}}{0}\right\}\to A{-}_{G}C=\underset{\dot{}}{0}$$
56	54 55	syl	$$⊢\phi \to A{-}_{G}C=\underset{\dot{}}{0}$$
57	22 2 13	grpsubeq0	$$⊢\left(G\in \mathrm{Grp}\wedge A\in {\mathrm{Base}}_G\wedge C\in {\mathrm{Base}}_G\right)\to \left(A{-}_{G}C=\underset{\dot{}}{0}\leftrightarrow A=C\right)$$
58	21 25 31 57	syl3anc	$$⊢\phi \to \left(A{-}_{G}C=\underset{\dot{}}{0}\leftrightarrow A=C\right)$$
59	56 58	mpbid	$$⊢\phi \to A=C$$