Theorem hlipcj

Description: Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hlipf.1	|- X = ( BaseSet ` U )
	hlipf.7	|- P = ( .iOLD ` U )
Assertion	hlipcj	|- ( ( U e. CHilOLD /\ A e. X /\ B e. X ) -> ( A P B ) = ( * ` ( B P A ) ) )

Proof

Step	Hyp	Ref	Expression
1		hlipf.1	|- X = ( BaseSet ` U )
2		hlipf.7	|- P = ( .iOLD ` U )
3		hlnv	|- ( U e. CHilOLD -> U e. NrmCVec )
4	1 2	dipcj	|- ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( * ` ( B P A ) ) = ( A P B ) )
5	3 4	syl3an1	|- ( ( U e. CHilOLD /\ B e. X /\ A e. X ) -> ( * ` ( B P A ) ) = ( A P B ) )
6	5	3com23	|- ( ( U e. CHilOLD /\ A e. X /\ B e. X ) -> ( * ` ( B P A ) ) = ( A P B ) )
7	6	eqcomd	|- ( ( U e. CHilOLD /\ A e. X /\ B e. X ) -> ( A P B ) = ( * ` ( B P A ) ) )