Metamath Proof Explorer

Theorem hoadddir

Description: Scalar product reverse distributive law for Hilbert space operators. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hoadddir ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) = ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) )

Proof

Step Hyp Ref Expression
1 addcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ด + ๐ต ) โˆˆ โ„‚ )
2 1 anim1i โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด + ๐ต ) โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) )
3 2 3impa โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด + ๐ต ) โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) )
4 homval โŠข ( ( ( ๐ด + ๐ต ) โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ( ๐ด + ๐ต ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
5 4 3expa โŠข ( ( ( ( ๐ด + ๐ต ) โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ( ๐ด + ๐ต ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
6 3 5 sylan โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ( ๐ด + ๐ต ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
7 homval โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
8 7 3expa โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
9 8 3adantl2 โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
10 homval โŠข ( ( ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ต ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ๐ต ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
11 10 3expa โŠข ( ( ( ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ต ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ๐ต ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
12 11 3adantl1 โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ต ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ๐ต ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
13 9 12 oveq12d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) +โ„Ž ( ( ๐ต ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) ) = ( ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) +โ„Ž ( ๐ต ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
14 ffvelcdm โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
15 ax-hvdistr2 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ ) โ†’ ( ( ๐ด + ๐ต ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) +โ„Ž ( ๐ต ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
16 14 15 syl3an3 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) ) โ†’ ( ( ๐ด + ๐ต ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) +โ„Ž ( ๐ต ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
17 16 3exp โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ต โˆˆ โ„‚ โ†’ ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด + ๐ต ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) +โ„Ž ( ๐ต ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ) ) )
18 17 exp4a โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ต โˆˆ โ„‚ โ†’ ( ๐‘‡ : โ„‹ โŸถ โ„‹ โ†’ ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( ๐ด + ๐ต ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) +โ„Ž ( ๐ต ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) ) ) ) )
19 18 3imp1 โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด + ๐ต ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) +โ„Ž ( ๐ต ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
20 13 19 eqtr4d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) +โ„Ž ( ( ๐ต ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) ) = ( ( ๐ด + ๐ต ) ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
21 6 20 eqtr4d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) +โ„Ž ( ( ๐ต ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) ) )
22 homulcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
23 homulcl โŠข ( ( ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ต ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
24 22 23 anim12i โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ๐ต ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ ) )
25 24 3impdir โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ๐ต ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ ) )
26 hosval โŠข ( ( ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ๐ต ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) +โ„Ž ( ( ๐ต ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) ) )
27 26 3expa โŠข ( ( ( ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ๐ต ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) +โ„Ž ( ( ๐ต ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) ) )
28 25 27 sylan โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) +โ„Ž ( ( ๐ต ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) ) )
29 21 28 eqtr4d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) โ€˜ ๐‘ฅ ) )
30 29 ralrimiva โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) โ€˜ ๐‘ฅ ) )
31 homulcl โŠข ( ( ( ๐ด + ๐ต ) โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
32 1 31 stoic3 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
33 hoaddcl โŠข ( ( ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ๐ต ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) : โ„‹ โŸถ โ„‹ )
34 22 23 33 syl2an โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) : โ„‹ โŸถ โ„‹ )
35 34 3impdir โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) : โ„‹ โŸถ โ„‹ )
36 hoeq โŠข ( ( ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) : โ„‹ โŸถ โ„‹ ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) โ€˜ ๐‘ฅ ) โ†” ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) = ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) ) )
37 32 35 36 syl2anc โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) โ€˜ ๐‘ฅ ) โ†” ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) = ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) ) )
38 30 37 mpbid โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด + ๐ต ) ยทop ๐‘‡ ) = ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ต ยทop ๐‘‡ ) ) )