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 | |
|
subgdisj.o | |
||
subgdisj.z | |
||
subgdisj.t | |
||
subgdisj.u | |
||
subgdisj.i | |
||
subgdisj.s | |
||
subgdisj.a | |
||
subgdisj.c | |
||
subgdisj.b | |
||
subgdisj.d | |
||
subgdisj.j | |
||
Assertion | subgdisj2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subgdisj.p | |
|
2 | subgdisj.o | |
|
3 | subgdisj.z | |
|
4 | subgdisj.t | |
|
5 | subgdisj.u | |
|
6 | subgdisj.i | |
|
7 | subgdisj.s | |
|
8 | subgdisj.a | |
|
9 | subgdisj.c | |
|
10 | subgdisj.b | |
|
11 | subgdisj.d | |
|
12 | subgdisj.j | |
|
13 | incom | |
|
14 | 13 6 | eqtr3id | |
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 | |