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