Metamath Proof Explorer


Theorem diporthcom

Description: Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ipcl.1
|- X = ( BaseSet ` U )
ipcl.7
|- P = ( .iOLD ` U )
Assertion diporthcom
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A P B ) = 0 <-> ( B P A ) = 0 ) )

Proof

Step Hyp Ref Expression
1 ipcl.1
 |-  X = ( BaseSet ` U )
2 ipcl.7
 |-  P = ( .iOLD ` U )
3 fveq2
 |-  ( ( A P B ) = 0 -> ( * ` ( A P B ) ) = ( * ` 0 ) )
4 cj0
 |-  ( * ` 0 ) = 0
5 3 4 eqtrdi
 |-  ( ( A P B ) = 0 -> ( * ` ( A P B ) ) = 0 )
6 1 2 dipcj
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( A P B ) ) = ( B P A ) )
7 6 eqeq1d
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( * ` ( A P B ) ) = 0 <-> ( B P A ) = 0 ) )
8 5 7 syl5ib
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A P B ) = 0 -> ( B P A ) = 0 ) )
9 fveq2
 |-  ( ( B P A ) = 0 -> ( * ` ( B P A ) ) = ( * ` 0 ) )
10 9 4 eqtrdi
 |-  ( ( B P A ) = 0 -> ( * ` ( B P A ) ) = 0 )
11 1 2 dipcj
 |-  ( ( U e. NrmCVec /\ B e. X /\ A e. X ) -> ( * ` ( B P A ) ) = ( A P B ) )
12 11 3com23
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( * ` ( B P A ) ) = ( A P B ) )
13 12 eqeq1d
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( * ` ( B P A ) ) = 0 <-> ( A P B ) = 0 ) )
14 10 13 syl5ib
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( B P A ) = 0 -> ( A P B ) = 0 ) )
15 8 14 impbid
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A P B ) = 0 <-> ( B P A ) = 0 ) )