Theorem his1i

Description: Conjugate law for inner product. Postulate (S1) of Beran p. 95. (Contributed by NM, 15-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	his1.1	$$⊢A\in \mathscr{H}$$
	his1.2	$$⊢B\in \mathscr{H}$$
Assertion	his1i	$$⊢A{\cdot }_{\mathrm{ih}}B=\overline{B{\cdot }_{\mathrm{ih}}A}$$

Proof

Step	Hyp	Ref	Expression
1		his1.1	$$⊢A\in \mathscr{H}$$
2		his1.2	$$⊢B\in \mathscr{H}$$
3		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}$$
4	1 2 3	mp2an	$$⊢A{\cdot }_{\mathrm{ih}}B=\overline{B{\cdot }_{\mathrm{ih}}A}$$