Metamath Proof Explorer

Theorem hmopco

Description: The composition of two commuting Hermitian operators is Hermitian. (Contributed by NM, 22-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopco ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp โˆง ( ๐‘‡ โˆ˜ ๐‘ˆ ) = ( ๐‘ˆ โˆ˜ ๐‘‡ ) ) โ†’ ( ๐‘‡ โˆ˜ ๐‘ˆ ) โˆˆ HrmOp )

Proof

Step Hyp Ref Expression
1 hmopf โŠข ( ๐‘‡ โˆˆ HrmOp โ†’ ๐‘‡ : โ„‹ โŸถ โ„‹ )
2 hmopf โŠข ( ๐‘ˆ โˆˆ HrmOp โ†’ ๐‘ˆ : โ„‹ โŸถ โ„‹ )
3 fco โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐‘‡ โˆ˜ ๐‘ˆ ) : โ„‹ โŸถ โ„‹ )
4 1 2 3 syl2an โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โ†’ ( ๐‘‡ โˆ˜ ๐‘ˆ ) : โ„‹ โŸถ โ„‹ )
5 4 3adant3 โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp โˆง ( ๐‘‡ โˆ˜ ๐‘ˆ ) = ( ๐‘ˆ โˆ˜ ๐‘‡ ) ) โ†’ ( ๐‘‡ โˆ˜ ๐‘ˆ ) : โ„‹ โŸถ โ„‹ )
6 fvco3 โŠข ( ( ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฆ ) = ( ๐‘‡ โ€˜ ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) )
7 2 6 sylan โŠข ( ( ๐‘ˆ โˆˆ HrmOp โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฆ ) = ( ๐‘‡ โ€˜ ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) )
8 7 oveq2d โŠข ( ( ๐‘ˆ โˆˆ HrmOp โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) )
9 8 ad2ant2l โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) )
10 simpll โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ๐‘‡ โˆˆ HrmOp )
11 simprl โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ๐‘ฅ โˆˆ โ„‹ )
12 2 ffvelcdmda โŠข ( ( ๐‘ˆ โˆˆ HrmOp โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ˆ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
13 12 ad2ant2l โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ˆ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
14 hmop โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹ โˆง ( ๐‘ˆ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) )
15 10 11 13 14 syl3anc โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ๐‘‡ โ€˜ ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) )
16 simplr โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ๐‘ˆ โˆˆ HrmOp )
17 1 ffvelcdmda โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
18 17 ad2ant2r โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
19 simprr โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ๐‘ฆ โˆˆ โ„‹ )
20 hmop โŠข ( ( ๐‘ˆ โˆˆ HrmOp โˆง ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ˆ โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฆ ) )
21 16 18 19 20 syl3anc โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ๐‘ˆ โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ˆ โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฆ ) )
22 9 15 21 3eqtrd โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ( ๐‘ˆ โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฆ ) )
23 fvco3 โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ๐‘ˆ โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
24 1 23 sylan โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ๐‘ˆ โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
25 24 oveq1d โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ๐‘ˆ โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฆ ) )
26 25 ad2ant2r โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ๐‘ˆ โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ยทih ๐‘ฆ ) )
27 22 26 eqtr4d โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ( ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
28 27 3adantl3 โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp โˆง ( ๐‘‡ โˆ˜ ๐‘ˆ ) = ( ๐‘ˆ โˆ˜ ๐‘‡ ) ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ( ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
29 fveq1 โŠข ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) = ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ†’ ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฅ ) = ( ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) )
30 29 oveq1d โŠข ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) = ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ†’ ( ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
31 30 3ad2ant3 โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp โˆง ( ๐‘‡ โˆ˜ ๐‘ˆ ) = ( ๐‘ˆ โˆ˜ ๐‘‡ ) ) โ†’ ( ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
32 31 adantr โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp โˆง ( ๐‘‡ โˆ˜ ๐‘ˆ ) = ( ๐‘ˆ โˆ˜ ๐‘‡ ) ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) = ( ( ( ๐‘ˆ โˆ˜ ๐‘‡ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
33 28 32 eqtr4d โŠข ( ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp โˆง ( ๐‘‡ โˆ˜ ๐‘ˆ ) = ( ๐‘ˆ โˆ˜ ๐‘‡ ) ) โˆง ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทih ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
34 33 ralrimivva โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp โˆง ( ๐‘‡ โˆ˜ ๐‘ˆ ) = ( ๐‘ˆ โˆ˜ ๐‘‡ ) ) โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) )
35 elhmop โŠข ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โˆˆ HrmOp โ†” ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ๐‘ฅ ยทih ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฆ ) ) = ( ( ( ๐‘‡ โˆ˜ ๐‘ˆ ) โ€˜ ๐‘ฅ ) ยทih ๐‘ฆ ) ) )
36 5 34 35 sylanbrc โŠข ( ( ๐‘‡ โˆˆ HrmOp โˆง ๐‘ˆ โˆˆ HrmOp โˆง ( ๐‘‡ โˆ˜ ๐‘ˆ ) = ( ๐‘ˆ โˆ˜ ๐‘‡ ) ) โ†’ ( ๐‘‡ โˆ˜ ๐‘ˆ ) โˆˆ HrmOp )