Metamath Proof Explorer

Theorem hmopd

Description: The difference of two Hermitian operators is Hermitian. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopd ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ โˆ’op ๐‘ˆ ) โˆˆ HrmOp )

Proof

Step Hyp Ref Expression
1 hmopf โŠข ( ๐‘‡ โˆˆ HrmOp โ†’ ๐‘‡ : โ„‹ โŸถ โ„‹ )
2 hmopf โŠข ( ๐‘ˆ โˆˆ HrmOp โ†’ ๐‘ˆ : โ„‹ โŸถ โ„‹ )
3 honegsub โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐‘‡ +op ( - 1 ยทop ๐‘ˆ ) ) = ( ๐‘‡ โˆ’op ๐‘ˆ ) )
4 1 2 3 syl2an โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ +op ( - 1 ยทop ๐‘ˆ ) ) = ( ๐‘‡ โˆ’op ๐‘ˆ ) )
5 neg1rr โŠข - 1 โˆˆ โ„
6 hmopm โŠข ( ( - 1 โˆˆ โ„ โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( - 1 ยทop ๐‘ˆ ) โˆˆ HrmOp )
7 5 6 mpan โŠข ( ๐‘ˆ โˆˆ HrmOp โ†’ ( - 1 ยทop ๐‘ˆ ) โˆˆ HrmOp )
8 hmops โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ( - 1 ยทop ๐‘ˆ ) โˆˆ HrmOp ) โ†’ ( ๐‘‡ +op ( - 1 ยทop ๐‘ˆ ) ) โˆˆ HrmOp )
9 7 8 sylan2 โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ +op ( - 1 ยทop ๐‘ˆ ) ) โˆˆ HrmOp )
10 4 9 eqeltrrd โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ โˆ’op ๐‘ˆ ) โˆˆ HrmOp )