Theorem iporthcom

Description: Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
	ip0l.z	$$⊢Z=0_F$$
Assertion	iporthcom	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{,}B=Z\leftrightarrow B\underset{\dot{}}{,}A=Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
4		ip0l.z	$$⊢Z=0_F$$
5	1	phlsrng	$$⊢W\in \mathrm{PreHil}\to F\in \mathrm{*-Ring}$$
6	5	3ad2ant1	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to F\in \mathrm{*-Ring}$$
7		eqid	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(F\right)={\ast }_{\mathrm{𝑟𝑓}}\left(F\right)$$
8		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
9	7 8	srngf1o	$$⊢F\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left(F\right):{\mathrm{Base}}_F\underset{1-1\; onto}{⟶}{\mathrm{Base}}_F$$
10		f1of1	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(F\right):{\mathrm{Base}}_F\underset{1-1\; onto}{⟶}{\mathrm{Base}}_F\to {\ast }_{\mathrm{𝑟𝑓}}\left(F\right):{\mathrm{Base}}_F\underset{1-1}{⟶}{\mathrm{Base}}_F$$
11	6 9 10	3syl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(F\right):{\mathrm{Base}}_F\underset{1-1}{⟶}{\mathrm{Base}}_F$$
12	1 2 3 8	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{,}B\in {\mathrm{Base}}_F$$
13		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
14	13	3ad2ant1	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to W\in \mathrm{LMod}$$
15	1 8 4	lmod0cl	$$⊢W\in \mathrm{LMod}\to Z\in {\mathrm{Base}}_F$$
16	14 15	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to Z\in {\mathrm{Base}}_F$$
17		f1fveq	$$⊢\left({\ast }_{\mathrm{𝑟𝑓}}\left(F\right):{\mathrm{Base}}_F\underset{1-1}{⟶}{\mathrm{Base}}_F\wedge \left(A\underset{\dot{}}{,}B\in {\mathrm{Base}}_F\wedge Z\in {\mathrm{Base}}_F\right)\right)\to \left({\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(A\underset{\dot{}}{,}B\right)={\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(Z\right)\leftrightarrow A\underset{\dot{}}{,}B=Z\right)$$
18	11 12 16 17	syl12anc	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left({\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(A\underset{\dot{}}{,}B\right)={\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(Z\right)\leftrightarrow A\underset{\dot{}}{,}B=Z\right)$$
19		eqid	$$⊢{\mathrm{*}}_F={\mathrm{*}}_F$$
20	8 19 7	stafval	$$⊢A\underset{\dot{}}{,}B\in {\mathrm{Base}}_F\to {\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(A\underset{\dot{}}{,}B\right)={\left(A\underset{\dot{}}{,}B\right)}^{{\mathrm{*}}_F}$$
21	12 20	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(A\underset{\dot{}}{,}B\right)={\left(A\underset{\dot{}}{,}B\right)}^{{\mathrm{*}}_F}$$
22	1 2 3 19	ipcj	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to {\left(A\underset{\dot{}}{,}B\right)}^{{\mathrm{*}}_F}=B\underset{\dot{}}{,}A$$
23	21 22	eqtrd	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(A\underset{\dot{}}{,}B\right)=B\underset{\dot{}}{,}A$$
24	8 19 7	stafval	$$⊢Z\in {\mathrm{Base}}_F\to {\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(Z\right)=Z^{{\mathrm{*}}_F}$$
25	16 24	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(Z\right)=Z^{{\mathrm{*}}_F}$$
26	19 4	srng0	$$⊢F\in \mathrm{*-Ring}\to Z^{{\mathrm{*}}_F}=Z$$
27	6 26	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to Z^{{\mathrm{*}}_F}=Z$$
28	25 27	eqtrd	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(Z\right)=Z$$
29	23 28	eqeq12d	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left({\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(A\underset{\dot{}}{,}B\right)={\ast }_{\mathrm{𝑟𝑓}}\left(F\right)\left(Z\right)\leftrightarrow B\underset{\dot{}}{,}A=Z\right)$$
30	18 29	bitr3d	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{,}B=Z\leftrightarrow B\underset{\dot{}}{,}A=Z\right)$$