Metamath Proof Explorer


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 ( 𝜑𝐵 = 𝐷 )