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 𝑋 = ( BaseSet ‘ 𝑈 )
ipcl.7 𝑃 = ( ·𝑖OLD𝑈 )
Assertion diporthcom ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝐴 𝑃 𝐵 ) = 0 ↔ ( 𝐵 𝑃 𝐴 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 ipcl.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 ipcl.7 𝑃 = ( ·𝑖OLD𝑈 )
3 fveq2 ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = ( ∗ ‘ 0 ) )
4 cj0 ( ∗ ‘ 0 ) = 0
5 3 4 eqtrdi ( ( 𝐴 𝑃 𝐵 ) = 0 → ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = 0 )
6 1 2 dipcj ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = ( 𝐵 𝑃 𝐴 ) )
7 6 eqeq1d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( ∗ ‘ ( 𝐴 𝑃 𝐵 ) ) = 0 ↔ ( 𝐵 𝑃 𝐴 ) = 0 ) )
8 5 7 syl5ib ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝐴 𝑃 𝐵 ) = 0 → ( 𝐵 𝑃 𝐴 ) = 0 ) )
9 fveq2 ( ( 𝐵 𝑃 𝐴 ) = 0 → ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = ( ∗ ‘ 0 ) )
10 9 4 eqtrdi ( ( 𝐵 𝑃 𝐴 ) = 0 → ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = 0 )
11 1 2 dipcj ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋𝐴𝑋 ) → ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = ( 𝐴 𝑃 𝐵 ) )
12 11 3com23 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = ( 𝐴 𝑃 𝐵 ) )
13 12 eqeq1d ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( ∗ ‘ ( 𝐵 𝑃 𝐴 ) ) = 0 ↔ ( 𝐴 𝑃 𝐵 ) = 0 ) )
14 10 13 syl5ib ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝐵 𝑃 𝐴 ) = 0 → ( 𝐴 𝑃 𝐵 ) = 0 ) )
15 8 14 impbid ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝐴 𝑃 𝐵 ) = 0 ↔ ( 𝐵 𝑃 𝐴 ) = 0 ) )