Metamath Proof Explorer

Theorem dipassr

Description: "Associative" law for second argument of inner product (compare dipass ). (Contributed by NM, 22-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 dipassr ⊢U∈CPreHilOLD∧A∈X∧B∈ℂ∧C∈X→APBSC=B‾⁢APC

Proof

Step Hyp Ref Expression
1 ipass.1 ⊢X=BaseSet⁡U
2 ipass.4 ⊢S=⋅𝑠OLD⁡U
3 ipass.7 ⊢P=⋅𝑖OLD⁡U
4 3anrot ⊢A∈X∧B∈ℂ∧C∈X↔B∈ℂ∧C∈X∧A∈X
5 1 2 3 dipass ⊢U∈CPreHilOLD∧B∈ℂ∧C∈X∧A∈X→BSCPA=B⁢CPA
6 4 5 sylan2b ⊢U∈CPreHilOLD∧A∈X∧B∈ℂ∧C∈X→BSCPA=B⁢CPA
7 6 fveq2d ⊢U∈CPreHilOLD∧A∈X∧B∈ℂ∧C∈X→BSCPA‾=B⁢CPA‾
8 phnv ⊢U∈CPreHilOLD→U∈NrmCVec
9 simpl ⊢U∈NrmCVec∧A∈X∧B∈ℂ∧C∈X→U∈NrmCVec
10 1 2 nvscl ⊢U∈NrmCVec∧B∈ℂ∧C∈X→BSC∈X
11 10 3adant3r1 ⊢U∈NrmCVec∧A∈X∧B∈ℂ∧C∈X→BSC∈X
12 simpr1 ⊢U∈NrmCVec∧A∈X∧B∈ℂ∧C∈X→A∈X
13 1 3 dipcj ⊢U∈NrmCVec∧BSC∈X∧A∈X→BSCPA‾=APBSC
14 9 11 12 13 syl3anc ⊢U∈NrmCVec∧A∈X∧B∈ℂ∧C∈X→BSCPA‾=APBSC
15 8 14 sylan ⊢U∈CPreHilOLD∧A∈X∧B∈ℂ∧C∈X→BSCPA‾=APBSC
16 simpr2 ⊢U∈NrmCVec∧A∈X∧B∈ℂ∧C∈X→B∈ℂ
17 1 3 dipcl ⊢U∈NrmCVec∧C∈X∧A∈X→CPA∈ℂ
18 17 3com23 ⊢U∈NrmCVec∧A∈X∧C∈X→CPA∈ℂ
19 18 3adant3r2 ⊢U∈NrmCVec∧A∈X∧B∈ℂ∧C∈X→CPA∈ℂ
20 16 19 cjmuld ⊢U∈NrmCVec∧A∈X∧B∈ℂ∧C∈X→B⁢CPA‾=B‾⁢CPA‾
21 1 3 dipcj ⊢U∈NrmCVec∧C∈X∧A∈X→CPA‾=APC
22 21 3com23 ⊢U∈NrmCVec∧A∈X∧C∈X→CPA‾=APC
23 22 3adant3r2 ⊢U∈NrmCVec∧A∈X∧B∈ℂ∧C∈X→CPA‾=APC
24 23 oveq2d ⊢U∈NrmCVec∧A∈X∧B∈ℂ∧C∈X→B‾⁢CPA‾=B‾⁢APC
25 20 24 eqtrd ⊢U∈NrmCVec∧A∈X∧B∈ℂ∧C∈X→B⁢CPA‾=B‾⁢APC
26 8 25 sylan ⊢U∈CPreHilOLD∧A∈X∧B∈ℂ∧C∈X→B⁢CPA‾=B‾⁢APC
27 7 15 26 3eqtr3d ⊢U∈CPreHilOLD∧A∈X∧B∈ℂ∧C∈X→APBSC=B‾⁢APC