Metamath Proof Explorer

Theorem ipdiri

Description: Distributive law for inner product. Equation I3 of Ponnusamy p. 362. (Contributed by NM, 27-Apr-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 ipdiri ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B P C = A P C + 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 oveq1 ⊢ A = if A ∈ X A 0 vec ⁡ U → A G B = if A ∈ X A 0 vec ⁡ U G B
7 6 oveq1d ⊢ A = if A ∈ X A 0 vec ⁡ U → A G B P C = if A ∈ X A 0 vec ⁡ U G B P C
8 oveq1 ⊢ A = if A ∈ X A 0 vec ⁡ U → A P C = if A ∈ X A 0 vec ⁡ U P C
9 8 oveq1d ⊢ A = if A ∈ X A 0 vec ⁡ U → A P C + B P C = if A ∈ X A 0 vec ⁡ U P C + B P C
10 7 9 eqeq12d ⊢ A = if A ∈ X A 0 vec ⁡ U → A G B P C = A P C + B P C ↔ if A ∈ X A 0 vec ⁡ U G B P C = if A ∈ X A 0 vec ⁡ U P C + B P C
11 oveq2 ⊢ B = if B ∈ X B 0 vec ⁡ U → if A ∈ X A 0 vec ⁡ U G B = if A ∈ X A 0 vec ⁡ U G if B ∈ X B 0 vec ⁡ U
12 11 oveq1d ⊢ B = if B ∈ X B 0 vec ⁡ U → if A ∈ X A 0 vec ⁡ U G B P C = if A ∈ X A 0 vec ⁡ U G if B ∈ X B 0 vec ⁡ U P C
13 oveq1 ⊢ B = if B ∈ X B 0 vec ⁡ U → B P C = if B ∈ X B 0 vec ⁡ U P C
14 13 oveq2d ⊢ B = if B ∈ X B 0 vec ⁡ U → if A ∈ X A 0 vec ⁡ U P C + B P C = if A ∈ X A 0 vec ⁡ U P C + if B ∈ X B 0 vec ⁡ U P C
15 12 14 eqeq12d ⊢ B = if B ∈ X B 0 vec ⁡ U → if A ∈ X A 0 vec ⁡ U G B P C = if A ∈ X A 0 vec ⁡ U P C + B P C ↔ if A ∈ X A 0 vec ⁡ U G if B ∈ X B 0 vec ⁡ U P C = if A ∈ X A 0 vec ⁡ U P C + if B ∈ X B 0 vec ⁡ U P C
16 oveq2 ⊢ C = if C ∈ X C 0 vec ⁡ U → if A ∈ X A 0 vec ⁡ U G if B ∈ X B 0 vec ⁡ U P C = if A ∈ X A 0 vec ⁡ U G if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U
17 oveq2 ⊢ C = if C ∈ X C 0 vec ⁡ U → if A ∈ X A 0 vec ⁡ U P C = if A ∈ X A 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U
18 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
19 17 18 oveq12d ⊢ C = if C ∈ X C 0 vec ⁡ U → if A ∈ X A 0 vec ⁡ U P C + if B ∈ X B 0 vec ⁡ U P C = if A ∈ X A 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U + if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U
20 16 19 eqeq12d ⊢ C = if C ∈ X C 0 vec ⁡ U → if A ∈ X A 0 vec ⁡ U G if B ∈ X B 0 vec ⁡ U P C = if A ∈ X A 0 vec ⁡ U P C + if B ∈ X B 0 vec ⁡ U P C ↔ if A ∈ X A 0 vec ⁡ U G if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U = if A ∈ X A 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U + if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U
21 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
22 1 21 5 elimph ⊢ if A ∈ X A 0 vec ⁡ U ∈ X
23 1 21 5 elimph ⊢ if B ∈ X B 0 vec ⁡ U ∈ X
24 1 21 5 elimph ⊢ if C ∈ X C 0 vec ⁡ U ∈ X
25 1 2 3 4 5 22 23 24 ipdirilem ⊢ if A ∈ X A 0 vec ⁡ U G if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U = if A ∈ X A 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U + if B ∈ X B 0 vec ⁡ U P if C ∈ X C 0 vec ⁡ U
26 10 15 20 25 dedth3h ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B P C = A P C + B P C