Metamath Proof Explorer

Theorem hmops

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

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

Proof

Step Hyp Ref Expression
1 hmopf โŠข ( ๐‘‡ โˆˆ HrmOp โ†’ ๐‘‡ : โ„‹ โŸถ โ„‹ )
2 hmopf โŠข ( ๐‘ˆ โˆˆ HrmOp โ†’ ๐‘ˆ : โ„‹ โŸถ โ„‹ )
3 hoaddcl โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐‘‡ +op ๐‘ˆ ) : โ„‹ โŸถ โ„‹ )
4 1 2 3 syl2an โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ +op ๐‘ˆ ) : โ„‹ โŸถ โ„‹ )
5 hmop โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
6 5 3expb โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
7 hmop โŠข ( ( ๐‘ˆ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
8 7 3expb โŠข ( ( ๐‘ˆ โˆˆ HrmOp โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
9 6 8 oveqan12d โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ( ๐‘ˆ โˆˆ HrmOp โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) ) โ†’ ( ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘ฅ ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) = ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) + ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) )
10 9 anandirs โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘ฅ ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) = ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) + ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) )
11 1 2 anim12i โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) )
12 hosval โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฆ ) = ( ( ๐‘‡ โ€˜ ๐‘ฆ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) )
13 12 oveq2d โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ๐‘ฅ ยทih ( ( ๐‘‡ โ€˜ ๐‘ฆ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) )
14 13 3expa โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ๐‘ฅ ยทih ( ( ๐‘‡ โ€˜ ๐‘ฆ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) )
15 14 adantrl โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ๐‘ฅ ยทih ( ( ๐‘‡ โ€˜ ๐‘ฆ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) )
16 simprl โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ๐‘ฅ โˆˆ โ„‹ )
17 ffvelcdm โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
18 17 ad2ant2rl โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
19 ffvelcdm โŠข ( ( ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ˆ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
20 19 ad2ant2l โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ˆ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
21 his7 โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( ๐‘‡ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ โˆง ( ๐‘ˆ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ โ€˜ ๐‘ฆ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) = ( ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘ฅ ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) )
22 16 18 20 21 syl3anc โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ โ€˜ ๐‘ฆ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) = ( ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘ฅ ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) )
23 15 22 eqtrd โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘ฅ ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) )
24 11 23 sylan โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘ฅ ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) )
25 hosval โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) )
26 25 oveq1d โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฆ ) )
27 26 3expa โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฆ ) )
28 27 adantrr โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฆ ) )
29 ffvelcdm โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
30 29 ad2ant2r โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
31 ffvelcdm โŠข ( ( ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐‘ˆ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
32 31 ad2ant2lr โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ˆ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
33 simprr โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ๐‘ฆ โˆˆ โ„‹ )
34 ax-his2 โŠข ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โˆง ( ๐‘ˆ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฆ ) = ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) + ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) )
35 30 32 33 34 syl3anc โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฆ ) = ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) + ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) )
36 28 35 eqtrd โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) + ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) )
37 11 36 sylan โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) + ( ( ๐‘ˆ โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) )
38 10 24 37 3eqtr4d โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
39 38 ralrimivva โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
40 elhmop โŠข ( ( ๐‘‡ +op ๐‘ˆ ) โˆˆ HrmOp โ†” ( ( ๐‘‡ +op ๐‘ˆ ) : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) )
41 4 39 40 sylanbrc โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ +op ๐‘ˆ ) โˆˆ HrmOp )