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 ) )