This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid ⊢ ( ( 𝑈 ∈ 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 imbitrid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐵 𝑃 𝐴 ) = 0 → ( 𝐴 𝑃 𝐵 ) = 0 ) )
15 8 14 impbid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑃 𝐵 ) = 0 ↔ ( 𝐵 𝑃 𝐴 ) = 0 ) )