Metamath Proof Explorer

Theorem honegdi

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 ๐‘ˆ ) ) )