This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cphipcj

Description: Conjugate of an inner product in a subcomplex pre-Hilbert space. Complex version of ipcj . (Contributed by Mario Carneiro, 16-Oct-2015)

		Ref	Expression
	Hypotheses	cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
		cphipcj.v	$⊢ V = {Base}_{W}$
	Assertion	cphipcj	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to \overline{A \underset{˙}{,} B} = B \underset{˙}{,} A$

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
2		cphipcj.v	$⊢ V = {Base}_{W}$
3		cphclm	$⊢ W \in CPreHil \to W \in CMod$
4		eqid	$⊢ Scalar (W) = Scalar (W)$
5	4	clmcj	$⊢ W \in CMod \to * = *_{Scalar (W)}$
6	3 5	syl	$⊢ W \in CPreHil \to * = *_{Scalar (W)}$
7	6	3ad2ant1	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to * = *_{Scalar (W)}$
8	7	fveq1d	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to \overline{A \underset{˙}{,} B} = {(A \underset{˙}{,} B)}^{*_{Scalar (W)}}$
9		cphphl	$⊢ W \in CPreHil \to W \in PreHil$
10		eqid	$⊢ _{Scalar (W)} = _{Scalar (W)}$
11	4 1 2 10	ipcj	$⊢ (W \in PreHil \land A \in V \land B \in V) \to {(A \underset{˙}{,} B)}^{*_{Scalar (W)}} = B \underset{˙}{,} A$
12	9 11	syl3an1	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to {(A \underset{˙}{,} B)}^{*_{Scalar (W)}} = B \underset{˙}{,} A$
13	8 12	eqtrd	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to \overline{A \underset{˙}{,} B} = B \underset{˙}{,} A$