Metamath Proof Explorer


Theorem abshicom

Description: Commuted inner products have the same absolute values. (Contributed by NM, 26-May-2006) (New usage is discouraged.)

Ref Expression
Assertion abshicom ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( abs โ€˜ ( ๐ด ยทih ๐ต ) ) = ( abs โ€˜ ( ๐ต ยทih ๐ด ) ) )

Proof

Step Hyp Ref Expression
1 ax-his1 โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ยทih ๐ต ) = ( โˆ— โ€˜ ( ๐ต ยทih ๐ด ) ) )
2 1 fveq2d โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( abs โ€˜ ( ๐ด ยทih ๐ต ) ) = ( abs โ€˜ ( โˆ— โ€˜ ( ๐ต ยทih ๐ด ) ) ) )
3 hicl โŠข ( ( ๐ต โˆˆ โ„‹ โˆง ๐ด โˆˆ โ„‹ ) โ†’ ( ๐ต ยทih ๐ด ) โˆˆ โ„‚ )
4 3 ancoms โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ต ยทih ๐ด ) โˆˆ โ„‚ )
5 4 abscjd โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( abs โ€˜ ( โˆ— โ€˜ ( ๐ต ยทih ๐ด ) ) ) = ( abs โ€˜ ( ๐ต ยทih ๐ด ) ) )
6 2 5 eqtrd โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( abs โ€˜ ( ๐ด ยทih ๐ต ) ) = ( abs โ€˜ ( ๐ต ยทih ๐ด ) ) )