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 ‘ 𝐺 )
	subgdisj.o	⊢ 0 = ( 0g ‘ 𝐺 )
	subgdisj.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	subgdisj.t	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
	subgdisj.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
	subgdisj.i	⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
	subgdisj.s	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
	subgdisj.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑇 )
	subgdisj.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
	subgdisj.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
	subgdisj.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
	subgdisj.j	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) )
Assertion	subgdisj2	⊢ ( 𝜑 → 𝐵 = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		subgdisj.p	⊢ + = ( +g ‘ 𝐺 )
2		subgdisj.o	⊢ 0 = ( 0g ‘ 𝐺 )
3		subgdisj.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4		subgdisj.t	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
5		subgdisj.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
6		subgdisj.i	⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
7		subgdisj.s	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
8		subgdisj.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑇 )
9		subgdisj.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
10		subgdisj.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
11		subgdisj.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
12		subgdisj.j	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) )
13		incom	⊢ ( 𝑇 ∩ 𝑈 ) = ( 𝑈 ∩ 𝑇 )
14	13 6	eqtr3id	⊢ ( 𝜑 → ( 𝑈 ∩ 𝑇 ) = { 0 } )
15	3 4 5 7	cntzrecd	⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) )
16	7 8	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑍 ‘ 𝑈 ) )
17	1 3	cntzi	⊢ ( ( 𝐴 ∈ ( 𝑍 ‘ 𝑈 ) ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
18	16 10 17	syl2anc	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
19	7 9	sseldd	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑍 ‘ 𝑈 ) )
20	1 3	cntzi	⊢ ( ( 𝐶 ∈ ( 𝑍 ‘ 𝑈 ) ∧ 𝐷 ∈ 𝑈 ) → ( 𝐶 + 𝐷 ) = ( 𝐷 + 𝐶 ) )
21	19 11 20	syl2anc	⊢ ( 𝜑 → ( 𝐶 + 𝐷 ) = ( 𝐷 + 𝐶 ) )
22	12 18 21	3eqtr3d	⊢ ( 𝜑 → ( 𝐵 + 𝐴 ) = ( 𝐷 + 𝐶 ) )
23	1 2 3 5 4 14 15 10 11 8 9 22	subgdisj1	⊢ ( 𝜑 → 𝐵 = 𝐷 )