Metamath Proof Explorer

Theorem hosub4

Description: Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hosub4 ( ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐‘… +op ๐‘† ) โˆ’op ( ๐‘‡ +op ๐‘ˆ ) ) = ( ( ๐‘… โˆ’op ๐‘‡ ) +op ( ๐‘† โˆ’op ๐‘ˆ ) ) )

Proof

Step Hyp Ref Expression
1 honegdi โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( - 1 ยทop ( ๐‘‡ +op ๐‘ˆ ) ) = ( ( - 1 ยทop ๐‘‡ ) +op ( - 1 ยทop ๐‘ˆ ) ) )
2 1 adantl โŠข ( ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( - 1 ยทop ( ๐‘‡ +op ๐‘ˆ ) ) = ( ( - 1 ยทop ๐‘‡ ) +op ( - 1 ยทop ๐‘ˆ ) ) )
3 2 oveq2d โŠข ( ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐‘… +op ๐‘† ) +op ( - 1 ยทop ( ๐‘‡ +op ๐‘ˆ ) ) ) = ( ( ๐‘… +op ๐‘† ) +op ( ( - 1 ยทop ๐‘‡ ) +op ( - 1 ยทop ๐‘ˆ ) ) ) )
4 neg1cn โŠข - 1 โˆˆ โ„‚
5 homulcl โŠข ( ( - 1 โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( - 1 ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
6 4 5 mpan โŠข ( ๐‘‡ : โ„‹ โŸถ โ„‹ โ†’ ( - 1 ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
7 homulcl โŠข ( ( - 1 โˆˆ โ„‚ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( - 1 ยทop ๐‘ˆ ) : โ„‹ โŸถ โ„‹ )
8 4 7 mpan โŠข ( ๐‘ˆ : โ„‹ โŸถ โ„‹ โ†’ ( - 1 ยทop ๐‘ˆ ) : โ„‹ โŸถ โ„‹ )
9 6 8 anim12i โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( - 1 ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( - 1 ยทop ๐‘ˆ ) : โ„‹ โŸถ โ„‹ ) )
10 hoadd4 โŠข ( ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โˆง ( ( - 1 ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( - 1 ยทop ๐‘ˆ ) : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐‘… +op ๐‘† ) +op ( ( - 1 ยทop ๐‘‡ ) +op ( - 1 ยทop ๐‘ˆ ) ) ) = ( ( ๐‘… +op ( - 1 ยทop ๐‘‡ ) ) +op ( ๐‘† +op ( - 1 ยทop ๐‘ˆ ) ) ) )
11 9 10 sylan2 โŠข ( ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐‘… +op ๐‘† ) +op ( ( - 1 ยทop ๐‘‡ ) +op ( - 1 ยทop ๐‘ˆ ) ) ) = ( ( ๐‘… +op ( - 1 ยทop ๐‘‡ ) ) +op ( ๐‘† +op ( - 1 ยทop ๐‘ˆ ) ) ) )
12 3 11 eqtrd โŠข ( ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐‘… +op ๐‘† ) +op ( - 1 ยทop ( ๐‘‡ +op ๐‘ˆ ) ) ) = ( ( ๐‘… +op ( - 1 ยทop ๐‘‡ ) ) +op ( ๐‘† +op ( - 1 ยทop ๐‘ˆ ) ) ) )
13 hoaddcl โŠข ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐‘… +op ๐‘† ) : โ„‹ โŸถ โ„‹ )
14 hoaddcl โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐‘‡ +op ๐‘ˆ ) : โ„‹ โŸถ โ„‹ )
15 honegsub โŠข ( ( ( ๐‘… +op ๐‘† ) : โ„‹ โŸถ โ„‹ โˆง ( ๐‘‡ +op ๐‘ˆ ) : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐‘… +op ๐‘† ) +op ( - 1 ยทop ( ๐‘‡ +op ๐‘ˆ ) ) ) = ( ( ๐‘… +op ๐‘† ) โˆ’op ( ๐‘‡ +op ๐‘ˆ ) ) )
16 13 14 15 syl2an โŠข ( ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐‘… +op ๐‘† ) +op ( - 1 ยทop ( ๐‘‡ +op ๐‘ˆ ) ) ) = ( ( ๐‘… +op ๐‘† ) โˆ’op ( ๐‘‡ +op ๐‘ˆ ) ) )
17 honegsub โŠข ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐‘… +op ( - 1 ยทop ๐‘‡ ) ) = ( ๐‘… โˆ’op ๐‘‡ ) )
18 17 ad2ant2r โŠข ( ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ๐‘… +op ( - 1 ยทop ๐‘‡ ) ) = ( ๐‘… โˆ’op ๐‘‡ ) )
19 honegsub โŠข ( ( ๐‘† : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐‘† +op ( - 1 ยทop ๐‘ˆ ) ) = ( ๐‘† โˆ’op ๐‘ˆ ) )
20 19 ad2ant2l โŠข ( ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ๐‘† +op ( - 1 ยทop ๐‘ˆ ) ) = ( ๐‘† โˆ’op ๐‘ˆ ) )
21 18 20 oveq12d โŠข ( ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐‘… +op ( - 1 ยทop ๐‘‡ ) ) +op ( ๐‘† +op ( - 1 ยทop ๐‘ˆ ) ) ) = ( ( ๐‘… โˆ’op ๐‘‡ ) +op ( ๐‘† โˆ’op ๐‘ˆ ) ) )
22 12 16 21 3eqtr3d โŠข ( ( ( ๐‘… : โ„‹ โŸถ โ„‹ โˆง ๐‘† : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐‘… +op ๐‘† ) โˆ’op ( ๐‘‡ +op ๐‘ˆ ) ) = ( ( ๐‘… โˆ’op ๐‘‡ ) +op ( ๐‘† โˆ’op ๐‘ˆ ) ) )