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∈CPreHilOLD
Assertion ipassi ⊢A∈ℂ∧B∈X∧C∈X→ASBPC=A⁢BPC

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∈CPreHilOLD
6 oveq2 ⊢B=ifB∈XB0vec⁡U→ASB=ASifB∈XB0vec⁡U
7 6 oveq1d ⊢B=ifB∈XB0vec⁡U→ASBPC=ASifB∈XB0vec⁡UPC
8 oveq1 ⊢B=ifB∈XB0vec⁡U→BPC=ifB∈XB0vec⁡UPC
9 8 oveq2d ⊢B=ifB∈XB0vec⁡U→A⁢BPC=A⁢ifB∈XB0vec⁡UPC
10 7 9 eqeq12d ⊢B=ifB∈XB0vec⁡U→ASBPC=A⁢BPC↔ASifB∈XB0vec⁡UPC=A⁢ifB∈XB0vec⁡UPC
11 10 imbi2d ⊢B=ifB∈XB0vec⁡U→A∈ℂ→ASBPC=A⁢BPC↔A∈ℂ→ASifB∈XB0vec⁡UPC=A⁢ifB∈XB0vec⁡UPC
12 oveq2 ⊢C=ifC∈XC0vec⁡U→ASifB∈XB0vec⁡UPC=ASifB∈XB0vec⁡UPifC∈XC0vec⁡U
13 oveq2 ⊢C=ifC∈XC0vec⁡U→ifB∈XB0vec⁡UPC=ifB∈XB0vec⁡UPifC∈XC0vec⁡U
14 13 oveq2d ⊢C=ifC∈XC0vec⁡U→A⁢ifB∈XB0vec⁡UPC=A⁢ifB∈XB0vec⁡UPifC∈XC0vec⁡U
15 12 14 eqeq12d ⊢C=ifC∈XC0vec⁡U→ASifB∈XB0vec⁡UPC=A⁢ifB∈XB0vec⁡UPC↔ASifB∈XB0vec⁡UPifC∈XC0vec⁡U=A⁢ifB∈XB0vec⁡UPifC∈XC0vec⁡U
16 15 imbi2d ⊢C=ifC∈XC0vec⁡U→A∈ℂ→ASifB∈XB0vec⁡UPC=A⁢ifB∈XB0vec⁡UPC↔A∈ℂ→ASifB∈XB0vec⁡UPifC∈XC0vec⁡U=A⁢ifB∈XB0vec⁡UPifC∈XC0vec⁡U
17 eqid ⊢0vec⁡U=0vec⁡U
18 1 17 5 elimph ⊢ifB∈XB0vec⁡U∈X
19 1 17 5 elimph ⊢ifC∈XC0vec⁡U∈X
20 1 2 3 4 5 18 19 ipasslem11 ⊢A∈ℂ→ASifB∈XB0vec⁡UPifC∈XC0vec⁡U=A⁢ifB∈XB0vec⁡UPifC∈XC0vec⁡U
21 11 16 20 dedth2h ⊢B∈X∧C∈X→A∈ℂ→ASBPC=A⁢BPC
22 21 com12 ⊢A∈ℂ→B∈X∧C∈X→ASBPC=A⁢BPC
23 22 3impib ⊢A∈ℂ∧B∈X∧C∈X→ASBPC=A⁢BPC