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	|- .+ = ( +g ` G )
	subgdisj.o	|- .0. = ( 0g ` G )
	subgdisj.z	|- Z = ( Cntz ` G )
	subgdisj.t	|- ( ph -> T e. ( SubGrp ` G ) )
	subgdisj.u	|- ( ph -> U e. ( SubGrp ` G ) )
	subgdisj.i	|- ( ph -> ( T i^i U ) = { .0. } )
	subgdisj.s	|- ( ph -> T C_ ( Z ` U ) )
	subgdisj.a	|- ( ph -> A e. T )
	subgdisj.c	|- ( ph -> C e. T )
	subgdisj.b	|- ( ph -> B e. U )
	subgdisj.d	|- ( ph -> D e. U )
	subgdisj.j	|- ( ph -> ( A .+ B ) = ( C .+ D ) )
Assertion	subgdisj2	|- ( ph -> B = D )

Proof

Step	Hyp	Ref	Expression
1		subgdisj.p	|- .+ = ( +g ` G )
2		subgdisj.o	|- .0. = ( 0g ` G )
3		subgdisj.z	|- Z = ( Cntz ` G )
4		subgdisj.t	|- ( ph -> T e. ( SubGrp ` G ) )
5		subgdisj.u	|- ( ph -> U e. ( SubGrp ` G ) )
6		subgdisj.i	|- ( ph -> ( T i^i U ) = { .0. } )
7		subgdisj.s	|- ( ph -> T C_ ( Z ` U ) )
8		subgdisj.a	|- ( ph -> A e. T )
9		subgdisj.c	|- ( ph -> C e. T )
10		subgdisj.b	|- ( ph -> B e. U )
11		subgdisj.d	|- ( ph -> D e. U )
12		subgdisj.j	|- ( ph -> ( A .+ B ) = ( C .+ D ) )
13		incom	|- ( T i^i U ) = ( U i^i T )
14	13 6	syl5eqr	|- ( ph -> ( U i^i T ) = { .0. } )
15	3 4 5 7	cntzrecd	|- ( ph -> U C_ ( Z ` T ) )
16	7 8	sseldd	|- ( ph -> A e. ( Z ` U ) )
17	1 3	cntzi	|- ( ( A e. ( Z ` U ) /\ B e. U ) -> ( A .+ B ) = ( B .+ A ) )
18	16 10 17	syl2anc	|- ( ph -> ( A .+ B ) = ( B .+ A ) )
19	7 9	sseldd	|- ( ph -> C e. ( Z ` U ) )
20	1 3	cntzi	|- ( ( C e. ( Z ` U ) /\ D e. U ) -> ( C .+ D ) = ( D .+ C ) )
21	19 11 20	syl2anc	|- ( ph -> ( C .+ D ) = ( D .+ C ) )
22	12 18 21	3eqtr3d	|- ( ph -> ( B .+ A ) = ( D .+ C ) )
23	1 2 3 5 4 14 15 10 11 8 9 22	subgdisj1	|- ( ph -> B = D )