Metamath Proof Explorer


Theorem brafnmul

Description: Anti-linearity property of bra functional for multiplication. (Contributed by NM, 31-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion brafnmul ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( bra โ€˜ ( ๐ด ยทโ„Ž ๐ต ) ) = ( ( โˆ— โ€˜ ๐ด ) ยทfn ( bra โ€˜ ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 hvmulcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ๐ต ) โˆˆ โ„‹ )
2 brafval โŠข ( ( ๐ด ยทโ„Ž ๐ต ) โˆˆ โ„‹ โ†’ ( bra โ€˜ ( ๐ด ยทโ„Ž ๐ต ) ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐‘ฅ ยทih ( ๐ด ยทโ„Ž ๐ต ) ) ) )
3 1 2 syl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( bra โ€˜ ( ๐ด ยทโ„Ž ๐ต ) ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐‘ฅ ยทih ( ๐ด ยทโ„Ž ๐ต ) ) ) )
4 cjcl โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( โˆ— โ€˜ ๐ด ) โˆˆ โ„‚ )
5 brafn โŠข ( ๐ต โˆˆ โ„‹ โ†’ ( bra โ€˜ ๐ต ) : โ„‹ โŸถ โ„‚ )
6 hfmmval โŠข ( ( ( โˆ— โ€˜ ๐ด ) โˆˆ โ„‚ โˆง ( bra โ€˜ ๐ต ) : โ„‹ โŸถ โ„‚ ) โ†’ ( ( โˆ— โ€˜ ๐ด ) ยทfn ( bra โ€˜ ๐ต ) ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ( โˆ— โ€˜ ๐ด ) ยท ( ( bra โ€˜ ๐ต ) โ€˜ ๐‘ฅ ) ) ) )
7 4 5 6 syl2an โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( โˆ— โ€˜ ๐ด ) ยทfn ( bra โ€˜ ๐ต ) ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ( โˆ— โ€˜ ๐ด ) ยท ( ( bra โ€˜ ๐ต ) โ€˜ ๐‘ฅ ) ) ) )
8 his5 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ๐ด ยทโ„Ž ๐ต ) ) = ( ( โˆ— โ€˜ ๐ด ) ยท ( ๐‘ฅ ยทih ๐ต ) ) )
9 8 3expa โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‹ ) โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ๐ด ยทโ„Ž ๐ต ) ) = ( ( โˆ— โ€˜ ๐ด ) ยท ( ๐‘ฅ ยทih ๐ต ) ) )
10 9 an32s โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ๐ด ยทโ„Ž ๐ต ) ) = ( ( โˆ— โ€˜ ๐ด ) ยท ( ๐‘ฅ ยทih ๐ต ) ) )
11 braval โŠข ( ( ๐ต โˆˆ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( bra โ€˜ ๐ต ) โ€˜ ๐‘ฅ ) = ( ๐‘ฅ ยทih ๐ต ) )
12 11 adantll โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( bra โ€˜ ๐ต ) โ€˜ ๐‘ฅ ) = ( ๐‘ฅ ยทih ๐ต ) )
13 12 oveq2d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ( โˆ— โ€˜ ๐ด ) ยท ( ( bra โ€˜ ๐ต ) โ€˜ ๐‘ฅ ) ) = ( ( โˆ— โ€˜ ๐ด ) ยท ( ๐‘ฅ ยทih ๐ต ) ) )
14 10 13 eqtr4d โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทih ( ๐ด ยทโ„Ž ๐ต ) ) = ( ( โˆ— โ€˜ ๐ด ) ยท ( ( bra โ€˜ ๐ต ) โ€˜ ๐‘ฅ ) ) )
15 14 mpteq2dva โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐‘ฅ ยทih ( ๐ด ยทโ„Ž ๐ต ) ) ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ( โˆ— โ€˜ ๐ด ) ยท ( ( bra โ€˜ ๐ต ) โ€˜ ๐‘ฅ ) ) ) )
16 7 15 eqtr4d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ( โˆ— โ€˜ ๐ด ) ยทfn ( bra โ€˜ ๐ต ) ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐‘ฅ ยทih ( ๐ด ยทโ„Ž ๐ต ) ) ) )
17 3 16 eqtr4d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( bra โ€˜ ( ๐ด ยทโ„Ž ๐ต ) ) = ( ( โˆ— โ€˜ ๐ด ) ยทfn ( bra โ€˜ ๐ต ) ) )