# Metamath Proof Explorer

## Theorem subgdisjb

Description: Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. Analogous to opth , this theorem shows a way of representing a pair of vectors. (Contributed by NM, 5-Jul-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses subgdisj.p
subgdisj.o
subgdisj.z ${⊢}{Z}=\mathrm{Cntz}\left({G}\right)$
subgdisj.t ${⊢}{\phi }\to {T}\in \mathrm{SubGrp}\left({G}\right)$
subgdisj.u ${⊢}{\phi }\to {U}\in \mathrm{SubGrp}\left({G}\right)$
subgdisj.i
subgdisj.s ${⊢}{\phi }\to {T}\subseteq {Z}\left({U}\right)$
subgdisj.a ${⊢}{\phi }\to {A}\in {T}$
subgdisj.c ${⊢}{\phi }\to {C}\in {T}$
subgdisj.b ${⊢}{\phi }\to {B}\in {U}$
subgdisj.d ${⊢}{\phi }\to {D}\in {U}$
Assertion subgdisjb

### Proof

Step Hyp Ref Expression
1 subgdisj.p
2 subgdisj.o
3 subgdisj.z ${⊢}{Z}=\mathrm{Cntz}\left({G}\right)$
4 subgdisj.t ${⊢}{\phi }\to {T}\in \mathrm{SubGrp}\left({G}\right)$
5 subgdisj.u ${⊢}{\phi }\to {U}\in \mathrm{SubGrp}\left({G}\right)$
6 subgdisj.i
7 subgdisj.s ${⊢}{\phi }\to {T}\subseteq {Z}\left({U}\right)$
8 subgdisj.a ${⊢}{\phi }\to {A}\in {T}$
9 subgdisj.c ${⊢}{\phi }\to {C}\in {T}$
10 subgdisj.b ${⊢}{\phi }\to {B}\in {U}$
11 subgdisj.d ${⊢}{\phi }\to {D}\in {U}$