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 Z=CntzG
subgdisj.t φTSubGrpG
subgdisj.u φUSubGrpG
subgdisj.i φTU=0˙
subgdisj.s φTZU
subgdisj.a φAT
subgdisj.c φCT
subgdisj.b φBU
subgdisj.d φDU
subgdisj.j φA+˙B=C+˙D
Assertion subgdisj2 φB=D

Proof

Step Hyp Ref Expression
1 subgdisj.p +˙=+G
2 subgdisj.o 0˙=0G
3 subgdisj.z Z=CntzG
4 subgdisj.t φTSubGrpG
5 subgdisj.u φUSubGrpG
6 subgdisj.i φTU=0˙
7 subgdisj.s φTZU
8 subgdisj.a φAT
9 subgdisj.c φCT
10 subgdisj.b φBU
11 subgdisj.d φDU
12 subgdisj.j φA+˙B=C+˙D
13 incom TU=UT
14 13 6 eqtr3id φUT=0˙
15 3 4 5 7 cntzrecd φUZT
16 7 8 sseldd φAZU
17 1 3 cntzi AZUBUA+˙B=B+˙A
18 16 10 17 syl2anc φA+˙B=B+˙A
19 7 9 sseldd φCZU
20 1 3 cntzi CZUDUC+˙D=D+˙C
21 19 11 20 syl2anc φC+˙D=D+˙C
22 12 18 21 3eqtr3d φB+˙A=D+˙C
23 1 2 3 5 4 14 15 10 11 8 9 22 subgdisj1 φB=D