Metamath Proof Explorer

Theorem hoadddi

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

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

Proof

Step Hyp Ref Expression
1 simpl1 โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ๐ด โˆˆ โ„‚ )
2 ffvelcdm โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
3 2 3ad2antl2 โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
4 ffvelcdm โŠข ( ( ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐‘ˆ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
5 4 3ad2antl3 โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐‘ˆ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
6 ax-hvdistr1 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ โˆง ( ๐‘ˆ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ) = ( ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) +โ„Ž ( ๐ด ยทโ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ) )
7 1 3 5 6 syl3anc โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ) = ( ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) +โ„Ž ( ๐ด ยทโ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ) )
8 hosval โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) = ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) )
9 8 oveq2d โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) = ( ๐ด ยทโ„Ž ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ) )
10 9 3expa โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) = ( ๐ด ยทโ„Ž ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ) )
11 10 3adantl1 โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) = ( ๐ด ยทโ„Ž ( ( ๐‘‡ โ€˜ ๐‘ฅ ) +โ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ) )
12 homval โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
13 12 3expa โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
14 13 3adantl3 โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
15 homval โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘ˆ ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) )
16 15 3expa โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘ˆ ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) )
17 16 3adantl2 โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘ˆ ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) )
18 14 17 oveq12d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) +โ„Ž ( ( ๐ด ยทop ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) = ( ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) +โ„Ž ( ๐ด ยทโ„Ž ( ๐‘ˆ โ€˜ ๐‘ฅ ) ) ) )
19 7 11 18 3eqtr4d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) = ( ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) +โ„Ž ( ( ๐ด ยทop ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) )
20 hoaddcl โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐‘‡ +op ๐‘ˆ ) : โ„‹ โŸถ โ„‹ )
21 20 anim2i โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ๐ด โˆˆ โ„‚ โˆง ( ๐‘‡ +op ๐‘ˆ ) : โ„‹ โŸถ โ„‹ ) )
22 21 3impb โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด โˆˆ โ„‚ โˆง ( ๐‘‡ +op ๐‘ˆ ) : โ„‹ โŸถ โ„‹ ) )
23 homval โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ( ๐‘‡ +op ๐‘ˆ ) : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) )
24 23 3expa โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ( ๐‘‡ +op ๐‘ˆ ) : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) )
25 22 24 sylan โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) = ( ๐ด ยทโ„Ž ( ( ๐‘‡ +op ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) )
26 homulcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
27 homulcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด ยทop ๐‘ˆ ) : โ„‹ โŸถ โ„‹ )
28 26 27 anim12i โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐ด โˆˆ โ„‚ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ๐ด ยทop ๐‘ˆ ) : โ„‹ โŸถ โ„‹ ) )
29 28 3impdi โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ๐ด ยทop ๐‘ˆ ) : โ„‹ โŸถ โ„‹ ) )
30 hosval โŠข ( ( ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ๐ด ยทop ๐‘ˆ ) : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) +โ„Ž ( ( ๐ด ยทop ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) )
31 30 3expa โŠข ( ( ( ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ๐ด ยทop ๐‘ˆ ) : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) +โ„Ž ( ( ๐ด ยทop ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) )
32 29 31 sylan โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) โ€˜ ๐‘ฅ ) +โ„Ž ( ( ๐ด ยทop ๐‘ˆ ) โ€˜ ๐‘ฅ ) ) )
33 19 25 32 3eqtr4d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) )
34 33 ralrimiva โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) )
35 homulcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ( ๐‘‡ +op ๐‘ˆ ) : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) : โ„‹ โŸถ โ„‹ )
36 20 35 sylan2 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) : โ„‹ โŸถ โ„‹ )
37 36 3impb โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) : โ„‹ โŸถ โ„‹ )
38 hoaddcl โŠข ( ( ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง ( ๐ด ยทop ๐‘ˆ ) : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) : โ„‹ โŸถ โ„‹ )
39 26 27 38 syl2an โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ( ๐ด โˆˆ โ„‚ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) : โ„‹ โŸถ โ„‹ )
40 39 3impdi โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) : โ„‹ โŸถ โ„‹ )
41 hoeq โŠข ( ( ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) : โ„‹ โŸถ โ„‹ โˆง ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) : โ„‹ โŸถ โ„‹ ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) โ†” ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) = ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) ) )
42 37 40 41 syl2anc โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) = ( ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) โ€˜ ๐‘ฅ ) โ†” ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) = ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) ) )
43 34 42 mpbid โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ˆ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด ยทop ( ๐‘‡ +op ๐‘ˆ ) ) = ( ( ๐ด ยทop ๐‘‡ ) +op ( ๐ด ยทop ๐‘ˆ ) ) )