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 ˙ = 0 G
subgdisj.z Z = Cntz G
subgdisj.t φ T SubGrp G
subgdisj.u φ U SubGrp G
subgdisj.i φ T U = 0 ˙
subgdisj.s φ T Z U
subgdisj.a φ A T
subgdisj.c φ C T
subgdisj.b φ B U
subgdisj.d φ D U
subgdisj.j φ A + ˙ B = C + ˙ D
Assertion subgdisj2 φ B = D

Proof

Step Hyp Ref Expression
1 subgdisj.p + ˙ = + G
2 subgdisj.o 0 ˙ = 0 G
3 subgdisj.z Z = Cntz G
4 subgdisj.t φ T SubGrp G
5 subgdisj.u φ U SubGrp G
6 subgdisj.i φ T U = 0 ˙
7 subgdisj.s φ T Z U
8 subgdisj.a φ A T
9 subgdisj.c φ C T
10 subgdisj.b φ B U
11 subgdisj.d φ D U
12 subgdisj.j φ A + ˙ B = C + ˙ D
13 incom T U = U T
14 13 6 eqtr3id φ U T = 0 ˙
15 3 4 5 7 cntzrecd φ U Z T
16 7 8 sseldd φ A Z U
17 1 3 cntzi A Z U B U A + ˙ B = B + ˙ A
18 16 10 17 syl2anc φ A + ˙ B = B + ˙ A
19 7 9 sseldd φ C Z U
20 1 3 cntzi C Z U D U C + ˙ 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