Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-vs | Structured version Visualization version GIF version |
Description: Define vector subtraction on a normed complex vector space. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-vs | ⊢ −𝑣 = ( /𝑔 ∘ +𝑣 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnsb 28670 | . 2 class −𝑣 | |
2 | cgs 28573 | . . 3 class /𝑔 | |
3 | cpv 28666 | . . 3 class +𝑣 | |
4 | 2, 3 | ccom 5555 | . 2 class ( /𝑔 ∘ +𝑣 ) |
5 | 1, 4 | wceq 1543 | 1 wff −𝑣 = ( /𝑔 ∘ +𝑣 ) |
Colors of variables: wff setvar class |
This definition is referenced by: vsfval 28714 |
Copyright terms: Public domain | W3C validator |