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 = ( Scalar ` W )
phllmhm.h
|- ., = ( .i ` W )
phllmhm.v
|- V = ( Base ` W )
ip0l.z
|- Z = ( 0g ` F )
Assertion iporthcom
|- ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( ( A ., B ) = Z <-> ( B ., A ) = Z ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f
 |-  F = ( Scalar ` W )
2 phllmhm.h
 |-  ., = ( .i ` W )
3 phllmhm.v
 |-  V = ( Base ` W )
4 ip0l.z
 |-  Z = ( 0g ` F )
5 1 phlsrng
 |-  ( W e. PreHil -> F e. *Ring )
6 5 3ad2ant1
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> F e. *Ring )
7 eqid
 |-  ( *rf ` F ) = ( *rf ` F )
8 eqid
 |-  ( Base ` F ) = ( Base ` F )
9 7 8 srngf1o
 |-  ( F e. *Ring -> ( *rf ` F ) : ( Base ` F ) -1-1-onto-> ( Base ` F ) )
10 f1of1
 |-  ( ( *rf ` F ) : ( Base ` F ) -1-1-onto-> ( Base ` F ) -> ( *rf ` F ) : ( Base ` F ) -1-1-> ( Base ` F ) )
11 6 9 10 3syl
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( *rf ` F ) : ( Base ` F ) -1-1-> ( Base ` F ) )
12 1 2 3 8 ipcl
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. ( Base ` F ) )
13 phllmod
 |-  ( W e. PreHil -> W e. LMod )
14 13 3ad2ant1
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> W e. LMod )
15 1 8 4 lmod0cl
 |-  ( W e. LMod -> Z e. ( Base ` F ) )
16 14 15 syl
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> Z e. ( Base ` F ) )
17 f1fveq
 |-  ( ( ( *rf ` F ) : ( Base ` F ) -1-1-> ( Base ` F ) /\ ( ( A ., B ) e. ( Base ` F ) /\ Z e. ( Base ` F ) ) ) -> ( ( ( *rf ` F ) ` ( A ., B ) ) = ( ( *rf ` F ) ` Z ) <-> ( A ., B ) = Z ) )
18 11 12 16 17 syl12anc
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( ( ( *rf ` F ) ` ( A ., B ) ) = ( ( *rf ` F ) ` Z ) <-> ( A ., B ) = Z ) )
19 eqid
 |-  ( *r ` F ) = ( *r ` F )
20 8 19 7 stafval
 |-  ( ( A ., B ) e. ( Base ` F ) -> ( ( *rf ` F ) ` ( A ., B ) ) = ( ( *r ` F ) ` ( A ., B ) ) )
21 12 20 syl
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( ( *rf ` F ) ` ( A ., B ) ) = ( ( *r ` F ) ` ( A ., B ) ) )
22 1 2 3 19 ipcj
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( ( *r ` F ) ` ( A ., B ) ) = ( B ., A ) )
23 21 22 eqtrd
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( ( *rf ` F ) ` ( A ., B ) ) = ( B ., A ) )
24 8 19 7 stafval
 |-  ( Z e. ( Base ` F ) -> ( ( *rf ` F ) ` Z ) = ( ( *r ` F ) ` Z ) )
25 16 24 syl
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( ( *rf ` F ) ` Z ) = ( ( *r ` F ) ` Z ) )
26 19 4 srng0
 |-  ( F e. *Ring -> ( ( *r ` F ) ` Z ) = Z )
27 6 26 syl
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( ( *r ` F ) ` Z ) = Z )
28 25 27 eqtrd
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( ( *rf ` F ) ` Z ) = Z )
29 23 28 eqeq12d
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( ( ( *rf ` F ) ` ( A ., B ) ) = ( ( *rf ` F ) ` Z ) <-> ( B ., A ) = Z ) )
30 18 29 bitr3d
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( ( A ., B ) = Z <-> ( B ., A ) = Z ) )