This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Distribution of negative over addition. (Contributed by NM, 24-Aug-2006)
(New usage is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
honegdi |
⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 +op 𝑈 ) ) = ( ( - 1 ·op 𝑇 ) +op ( - 1 ·op 𝑈 ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
| 2 |
|
hoadddi |
⊢ ( ( - 1 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 +op 𝑈 ) ) = ( ( - 1 ·op 𝑇 ) +op ( - 1 ·op 𝑈 ) ) ) |
| 3 |
1 2
|
mp3an1 |
⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 +op 𝑈 ) ) = ( ( - 1 ·op 𝑇 ) +op ( - 1 ·op 𝑈 ) ) ) |