Metamath Proof Explorer

Theorem ipcj

Description: Conjugate of an inner product in a pre-Hilbert space. Equation I1 of Ponnusamy p. 362. (Contributed by NM, 1-Feb-2007) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ipcj.i ⊢ ∗ = ( *𝑟 ‘ 𝐹 )
Assertion ipcj ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∗ ‘ ( 𝐴 , 𝐵 ) ) = ( 𝐵 , 𝐴 ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 ipcj.i ⊢ ∗ = ( *𝑟 ‘ 𝐹 )
5 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
6 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
7 3 1 2 5 4 6 isphl ⊢ ( 𝑊 ∈ PreHil ↔ ( 𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = ( 0g ‘ 𝐹 ) → 𝑥 = ( 0g ‘ 𝑊 ) ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) )
8 7 simp3bi ⊢ ( 𝑊 ∈ PreHil → ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = ( 0g ‘ 𝐹 ) → 𝑥 = ( 0g ‘ 𝑊 ) ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) )
9 simp3 ⊢ ( ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = ( 0g ‘ 𝐹 ) → 𝑥 = ( 0g ‘ 𝑊 ) ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) → ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) )
10 9 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = ( 0g ‘ 𝐹 ) → 𝑥 = ( 0g ‘ 𝑊 ) ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) )
11 8 10 syl ⊢ ( 𝑊 ∈ PreHil → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) )
12 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( ∗ ‘ ( 𝐴 , 𝑦 ) ) )
13 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑦 , 𝑥 ) = ( 𝑦 , 𝐴 ) )
14 12 13 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ↔ ( ∗ ‘ ( 𝐴 , 𝑦 ) ) = ( 𝑦 , 𝐴 ) ) )
15 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 , 𝑦 ) = ( 𝐴 , 𝐵 ) )
16 15 fveq2d ⊢ ( 𝑦 = 𝐵 → ( ∗ ‘ ( 𝐴 , 𝑦 ) ) = ( ∗ ‘ ( 𝐴 , 𝐵 ) ) )
17 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 , 𝐴 ) = ( 𝐵 , 𝐴 ) )
18 16 17 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( ∗ ‘ ( 𝐴 , 𝑦 ) ) = ( 𝑦 , 𝐴 ) ↔ ( ∗ ‘ ( 𝐴 , 𝐵 ) ) = ( 𝐵 , 𝐴 ) ) )
19 14 18 rspc2v ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) → ( ∗ ‘ ( 𝐴 , 𝐵 ) ) = ( 𝐵 , 𝐴 ) ) )
20 11 19 syl5com ⊢ ( 𝑊 ∈ PreHil → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∗ ‘ ( 𝐴 , 𝐵 ) ) = ( 𝐵 , 𝐴 ) ) )
21 20 3impib ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∗ ‘ ( 𝐴 , 𝐵 ) ) = ( 𝐵 , 𝐴 ) )