Metamath Proof Explorer

Theorem ipassi

Description: Associative law for inner product. Equation I2 of Ponnusamy p. 363. (Contributed by NM, 25-Aug-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 ⊢ X = BaseSet ⁡ U
ip1i.2 ⊢ G = + v ⁡ U
ip1i.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
ip1i.9 ⊢ U ∈ CPreHil OLD
Assertion ipassi ⊢ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A S B P C = A ⁢ B P C

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢ X = BaseSet ⁡ U
2 ip1i.2 ⊢ G = + v ⁡ U
3 ip1i.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 ip1i.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
5 ip1i.9 ⊢ U ∈ CPreHil OLD
6 oveq2 ⊢ B = if B ∈ X B 0 vec ⁡ U → A S B = A S if B ∈ X B 0 vec ⁡ U
7 6 oveq1d ⊢ B = if B ∈ X B 0 vec ⁡ U → A S B P C = A S if B ∈ X B 0 vec ⁡ U P C
8 oveq1 ⊢ B = if B ∈ X B 0 vec ⁡ U → B P C = if B ∈ X B 0 vec ⁡ U P C
9 8 oveq2d ⊢ B = if B ∈ X B 0 vec ⁡ U → A ⁢ B P C = A ⁢ if B ∈ X B 0 vec ⁡ U P C
10 7 9 eqeq12d ⊢ B = if B ∈ X B 0 vec ⁡ U → A S B P C = A ⁢ B P C ↔ A S if B ∈ X B 0 vec ⁡ U P C = A ⁢ if B ∈ X B 0 vec ⁡ U P C
11 10 imbi2d ⊢ B = if B ∈ X B 0 vec ⁡ U → A ∈ ℂ → A S B P C = A ⁢ B P C ↔ A ∈ ℂ → A S if B ∈ X B 0 vec ⁡ U P C = A ⁢ if B ∈ X B 0 vec ⁡ U P C
12 oveq2 ⊢ C = if C ∈ X C 0 vec ⁡ U → A S if B ∈ X B 0 vec ⁡ U P C = A S if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U
13 oveq2 ⊢ C = if C ∈ X C 0 vec ⁡ U → if B ∈ X B 0 vec ⁡ U P C = if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U
14 13 oveq2d ⊢ C = if C ∈ X C 0 vec ⁡ U → A ⁢ if B ∈ X B 0 vec ⁡ U P C = A ⁢ if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U
15 12 14 eqeq12d ⊢ C = if C ∈ X C 0 vec ⁡ U → A S if B ∈ X B 0 vec ⁡ U P C = A ⁢ if B ∈ X B 0 vec ⁡ U P C ↔ A S if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U = A ⁢ if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U
16 15 imbi2d ⊢ C = if C ∈ X C 0 vec ⁡ U → A ∈ ℂ → A S if B ∈ X B 0 vec ⁡ U P C = A ⁢ if B ∈ X B 0 vec ⁡ U P C ↔ A ∈ ℂ → A S if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U = A ⁢ if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U
17 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
18 1 17 5 elimph ⊢ if B ∈ X B 0 vec ⁡ U ∈ X
19 1 17 5 elimph ⊢ if C ∈ X C 0 vec ⁡ U ∈ X
20 1 2 3 4 5 18 19 ipasslem11 ⊢ A ∈ ℂ → A S if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U = A ⁢ if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U
21 11 16 20 dedth2h ⊢ B ∈ X ∧ C ∈ X → A ∈ ℂ → A S B P C = A ⁢ B P C
22 21 com12 ⊢ A ∈ ℂ → B ∈ X ∧ C ∈ X → A S B P C = A ⁢ B P C
23 22 3impib ⊢ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A S B P C = A ⁢ B P C