# Metamath Proof Explorer

## 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
phllmhm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
ip0l.z ${⊢}{Z}={0}_{{F}}$
Assertion iporthcom

### Proof

Step Hyp Ref Expression
1 phlsrng.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
2 phllmhm.h
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
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
18 11 12 16 17 syl12anc
19 eqid ${⊢}{*}_{{F}}={*}_{{F}}$
20 8 19 7 stafval
21 12 20 syl
22 1 2 3 19 ipcj
23 21 22 eqtrd
24 8 19 7 stafval ${⊢}{Z}\in {\mathrm{Base}}_{{F}}\to {\ast }_{\mathrm{𝑟𝑓}}\left({F}\right)\left({Z}\right)={{Z}}^{{*}_{{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}}^{{*}_{{F}}}$
26 19 4 srng0 ${⊢}{F}\in \mathrm{*-Ring}\to {{Z}}^{{*}_{{F}}}={Z}$
27 6 26 syl ${⊢}\left({W}\in \mathrm{PreHil}\wedge {A}\in {V}\wedge {B}\in {V}\right)\to {{Z}}^{{*}_{{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
30 18 29 bitr3d