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	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left|A{\cdot }_{\mathrm{ih}}B\right|=\left|B{\cdot }_{\mathrm{ih}}A\right|$$

Proof

Step	Hyp	Ref	Expression
1		ax-his1	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{\cdot }_{\mathrm{ih}}B=\overline{B{\cdot }_{\mathrm{ih}}A}$$
2	1	fveq2d	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left|A{\cdot }_{\mathrm{ih}}B\right|=\left|\overline{B{\cdot }_{\mathrm{ih}}A}\right|$$
3		hicl	$$⊢\left(B\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to B{\cdot }_{\mathrm{ih}}A\in ℂ$$
4	3	ancoms	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to B{\cdot }_{\mathrm{ih}}A\in ℂ$$
5	4	abscjd	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left|\overline{B{\cdot }_{\mathrm{ih}}A}\right|=\left|B{\cdot }_{\mathrm{ih}}A\right|$$
6	2 5	eqtrd	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left|A{\cdot }_{\mathrm{ih}}B\right|=\left|B{\cdot }_{\mathrm{ih}}A\right|$$