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 = ⋅ 𝑖OLD ⁡ U
Assertion diporthcom ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B = 0 ↔ B P A = 0

Proof

Step Hyp Ref Expression
1 ipcl.1 ⊢ X = BaseSet ⁡ U
2 ipcl.7 ⊢ P = ⋅ 𝑖OLD ⁡ 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 ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ‾ = B P A
7 6 eqeq1d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B ‾ = 0 ↔ B P A = 0
8 5 7 imbitrid ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ 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 ∈ NrmCVec ∧ B ∈ X ∧ A ∈ X → B P A ‾ = A P B
12 11 3com23 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → B P A ‾ = A P B
13 12 eqeq1d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → B P A ‾ = 0 ↔ A P B = 0
14 10 13 imbitrid ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → B P A = 0 → A P B = 0
15 8 14 impbid ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A P B = 0 ↔ B P A = 0