Metamath Proof Explorer

Theorem dipassr2

Description: "Associative" law for inner product. Conjugate version of dipassr . (Contributed by NM, 23-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipass.1 ⊢ X = BaseSet ⁡ U
ipass.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
ipass.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
Assertion dipassr2 ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ ℂ ∧ C ∈ X → A P B ‾ S C = B ⁢ A P C

Proof

Step Hyp Ref Expression
1 ipass.1 ⊢ X = BaseSet ⁡ U
2 ipass.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
3 ipass.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
4 cjcl ⊢ B ∈ ℂ → B ‾ ∈ ℂ
5 1 2 3 dipassr ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ‾ ∈ ℂ ∧ C ∈ X → A P B ‾ S C = B ‾ ‾ ⁢ A P C
6 4 5 syl3anr2 ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ ℂ ∧ C ∈ X → A P B ‾ S C = B ‾ ‾ ⁢ A P C
7 cjcj ⊢ B ∈ ℂ → B ‾ ‾ = B
8 7 3ad2ant2 ⊢ A ∈ X ∧ B ∈ ℂ ∧ C ∈ X → B ‾ ‾ = B
9 8 adantl ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ ℂ ∧ C ∈ X → B ‾ ‾ = B
10 9 oveq1d ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ ℂ ∧ C ∈ X → B ‾ ‾ ⁢ A P C = B ⁢ A P C
11 6 10 eqtrd ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ ℂ ∧ C ∈ X → A P B ‾ S C = B ⁢ A P C