Metamath Proof Explorer

Theorem honegsubdi2

Description: Distribution of negative over subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion honegsubdi2 ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( - 1 ยทop ( ๐‘‡ โˆ’op ๐‘ˆ ) ) = ( ๐‘ˆ โˆ’op ๐‘‡ ) )

Proof

Step Hyp Ref Expression
1 honegsubdi โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( - 1 ยทop ( ๐‘‡ โˆ’op ๐‘ˆ ) ) = ( ( - 1 ยทop ๐‘‡ ) +op ๐‘ˆ ) )
2 neg1cn โŠข - 1 โˆˆ โ„‚
3 homulcl โŠข ( ( - 1 โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( - 1 ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
4 2 3 mpan โŠข ( ๐‘‡ : โ„‹ โŸถ โ„‹ โ†’ ( - 1 ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
5 hoaddcom โŠข ( ( ( - 1 ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( - 1 ยทop ๐‘‡ ) +op ๐‘ˆ ) = ( ๐‘ˆ +op ( - 1 ยทop ๐‘‡ ) ) )
6 4 5 sylan โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( - 1 ยทop ๐‘‡ ) +op ๐‘ˆ ) = ( ๐‘ˆ +op ( - 1 ยทop ๐‘‡ ) ) )
7 honegsub โŠข ( ( ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐‘ˆ +op ( - 1 ยทop ๐‘‡ ) ) = ( ๐‘ˆ โˆ’op ๐‘‡ ) )
8 7 ancoms โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐‘ˆ +op ( - 1 ยทop ๐‘‡ ) ) = ( ๐‘ˆ โˆ’op ๐‘‡ ) )
9 1 6 8 3eqtrd โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( - 1 ยทop ( ๐‘‡ โˆ’op ๐‘ˆ ) ) = ( ๐‘ˆ โˆ’op ๐‘‡ ) )