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