Metamath Proof Explorer

Theorem iporthcom

Description: Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ip0l.z ⊢ 𝑍 = ( 0g ‘ 𝐹 )
Assertion iporthcom ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) = 𝑍 ↔ ( 𝐵 , 𝐴 ) = 𝑍 ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 ip0l.z ⊢ 𝑍 = ( 0g ‘ 𝐹 )
5 1 phlsrng ⊢ ( 𝑊 ∈ PreHil → 𝐹 ∈ *-Ring )
6 5 3ad2ant1 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐹 ∈ *-Ring )
7 eqid ⊢ ( *rf ‘ 𝐹 ) = ( *rf ‘ 𝐹 )
8 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
9 7 8 srngf1o ⊢ ( 𝐹 ∈ *-Ring → ( *rf ‘ 𝐹 ) : ( Base ‘ 𝐹 ) –1-1-onto→ ( Base ‘ 𝐹 ) )
10 f1of1 ⊢ ( ( *rf ‘ 𝐹 ) : ( Base ‘ 𝐹 ) –1-1-onto→ ( Base ‘ 𝐹 ) → ( *rf ‘ 𝐹 ) : ( Base ‘ 𝐹 ) –1-1→ ( Base ‘ 𝐹 ) )
11 6 9 10 3syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( *rf ‘ 𝐹 ) : ( Base ‘ 𝐹 ) –1-1→ ( Base ‘ 𝐹 ) )
12 1 2 3 8 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ ( Base ‘ 𝐹 ) )
13 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
14 13 3ad2ant1 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑊 ∈ LMod )
15 1 8 4 lmod0cl ⊢ ( 𝑊 ∈ LMod → 𝑍 ∈ ( Base ‘ 𝐹 ) )
16 14 15 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑍 ∈ ( Base ‘ 𝐹 ) )
17 f1fveq ⊢ ( ( ( *rf ‘ 𝐹 ) : ( Base ‘ 𝐹 ) –1-1→ ( Base ‘ 𝐹 ) ∧ ( ( 𝐴 , 𝐵 ) ∈ ( Base ‘ 𝐹 ) ∧ 𝑍 ∈ ( Base ‘ 𝐹 ) ) ) → ( ( ( *rf ‘ 𝐹 ) ‘ ( 𝐴 , 𝐵 ) ) = ( ( *rf ‘ 𝐹 ) ‘ 𝑍 ) ↔ ( 𝐴 , 𝐵 ) = 𝑍 ) )
18 11 12 16 17 syl12anc ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( *rf ‘ 𝐹 ) ‘ ( 𝐴 , 𝐵 ) ) = ( ( *rf ‘ 𝐹 ) ‘ 𝑍 ) ↔ ( 𝐴 , 𝐵 ) = 𝑍 ) )
19 eqid ⊢ ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ 𝐹 )
20 8 19 7 stafval ⊢ ( ( 𝐴 , 𝐵 ) ∈ ( Base ‘ 𝐹 ) → ( ( *rf ‘ 𝐹 ) ‘ ( 𝐴 , 𝐵 ) ) = ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐴 , 𝐵 ) ) )
21 12 20 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( *rf ‘ 𝐹 ) ‘ ( 𝐴 , 𝐵 ) ) = ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐴 , 𝐵 ) ) )
22 1 2 3 19 ipcj ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐴 , 𝐵 ) ) = ( 𝐵 , 𝐴 ) )
23 21 22 eqtrd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( *rf ‘ 𝐹 ) ‘ ( 𝐴 , 𝐵 ) ) = ( 𝐵 , 𝐴 ) )
24 8 19 7 stafval ⊢ ( 𝑍 ∈ ( Base ‘ 𝐹 ) → ( ( *rf ‘ 𝐹 ) ‘ 𝑍 ) = ( ( *𝑟 ‘ 𝐹 ) ‘ 𝑍 ) )
25 16 24 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( *rf ‘ 𝐹 ) ‘ 𝑍 ) = ( ( *𝑟 ‘ 𝐹 ) ‘ 𝑍 ) )
26 19 4 srng0 ⊢ ( 𝐹 ∈ *-Ring → ( ( *𝑟 ‘ 𝐹 ) ‘ 𝑍 ) = 𝑍 )
27 6 26 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ 𝑍 ) = 𝑍 )
28 25 27 eqtrd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( *rf ‘ 𝐹 ) ‘ 𝑍 ) = 𝑍 )
29 23 28 eqeq12d ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( *rf ‘ 𝐹 ) ‘ ( 𝐴 , 𝐵 ) ) = ( ( *rf ‘ 𝐹 ) ‘ 𝑍 ) ↔ ( 𝐵 , 𝐴 ) = 𝑍 ) )
30 18 29 bitr3d ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 , 𝐵 ) = 𝑍 ↔ ( 𝐵 , 𝐴 ) = 𝑍 ) )