Metamath Proof Explorer


Theorem dipdir

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

Ref Expression
Hypotheses dipdir.1 X = BaseSet U
dipdir.2 G = + v U
dipdir.7 P = 𝑖OLD U
Assertion dipdir U CPreHil OLD A X B X C X A G B P C = A P C + B P C

Proof

Step Hyp Ref Expression
1 dipdir.1 X = BaseSet U
2 dipdir.2 G = + v U
3 dipdir.7 P = 𝑖OLD U
4 fveq2 U = if U CPreHil OLD U + × abs BaseSet U = BaseSet if U CPreHil OLD U + × abs
5 1 4 syl5eq U = if U CPreHil OLD U + × abs X = BaseSet if U CPreHil OLD U + × abs
6 5 eleq2d U = if U CPreHil OLD U + × abs A X A BaseSet if U CPreHil OLD U + × abs
7 5 eleq2d U = if U CPreHil OLD U + × abs B X B BaseSet if U CPreHil OLD U + × abs
8 5 eleq2d U = if U CPreHil OLD U + × abs C X C BaseSet if U CPreHil OLD U + × abs
9 6 7 8 3anbi123d U = if U CPreHil OLD U + × abs A X B X C X A BaseSet if U CPreHil OLD U + × abs B BaseSet if U CPreHil OLD U + × abs C BaseSet if U CPreHil OLD U + × abs
10 fveq2 U = if U CPreHil OLD U + × abs + v U = + v if U CPreHil OLD U + × abs
11 2 10 syl5eq U = if U CPreHil OLD U + × abs G = + v if U CPreHil OLD U + × abs
12 11 oveqd U = if U CPreHil OLD U + × abs A G B = A + v if U CPreHil OLD U + × abs B
13 12 oveq1d U = if U CPreHil OLD U + × abs A G B P C = A + v if U CPreHil OLD U + × abs B P C
14 fveq2 U = if U CPreHil OLD U + × abs 𝑖OLD U = 𝑖OLD if U CPreHil OLD U + × abs
15 3 14 syl5eq U = if U CPreHil OLD U + × abs P = 𝑖OLD if U CPreHil OLD U + × abs
16 15 oveqd U = if U CPreHil OLD U + × abs A + v if U CPreHil OLD U + × abs B P C = A + v if U CPreHil OLD U + × abs B 𝑖OLD if U CPreHil OLD U + × abs C
17 13 16 eqtrd U = if U CPreHil OLD U + × abs A G B P C = A + v if U CPreHil OLD U + × abs B 𝑖OLD if U CPreHil OLD U + × abs C
18 15 oveqd U = if U CPreHil OLD U + × abs A P C = A 𝑖OLD if U CPreHil OLD U + × abs C
19 15 oveqd U = if U CPreHil OLD U + × abs B P C = B 𝑖OLD if U CPreHil OLD U + × abs C
20 18 19 oveq12d U = if U CPreHil OLD U + × abs A P C + B P C = A 𝑖OLD if U CPreHil OLD U + × abs C + B 𝑖OLD if U CPreHil OLD U + × abs C
21 17 20 eqeq12d U = if U CPreHil OLD U + × abs A G B P C = A P C + B P C A + v if U CPreHil OLD U + × abs B 𝑖OLD if U CPreHil OLD U + × abs C = A 𝑖OLD if U CPreHil OLD U + × abs C + B 𝑖OLD if U CPreHil OLD U + × abs C
22 9 21 imbi12d U = if U CPreHil OLD U + × abs A X B X C X A G B P C = A P C + B P C A BaseSet if U CPreHil OLD U + × abs B BaseSet if U CPreHil OLD U + × abs C BaseSet if U CPreHil OLD U + × abs A + v if U CPreHil OLD U + × abs B 𝑖OLD if U CPreHil OLD U + × abs C = A 𝑖OLD if U CPreHil OLD U + × abs C + B 𝑖OLD if U CPreHil OLD U + × abs C
23 eqid BaseSet if U CPreHil OLD U + × abs = BaseSet if U CPreHil OLD U + × abs
24 eqid + v if U CPreHil OLD U + × abs = + v if U CPreHil OLD U + × abs
25 eqid 𝑠OLD if U CPreHil OLD U + × abs = 𝑠OLD if U CPreHil OLD U + × abs
26 eqid 𝑖OLD if U CPreHil OLD U + × abs = 𝑖OLD if U CPreHil OLD U + × abs
27 elimphu if U CPreHil OLD U + × abs CPreHil OLD
28 23 24 25 26 27 ipdiri A BaseSet if U CPreHil OLD U + × abs B BaseSet if U CPreHil OLD U + × abs C BaseSet if U CPreHil OLD U + × abs A + v if U CPreHil OLD U + × abs B 𝑖OLD if U CPreHil OLD U + × abs C = A 𝑖OLD if U CPreHil OLD U + × abs C + B 𝑖OLD if U CPreHil OLD U + × abs C
29 22 28 dedth U CPreHil OLD A X B X C X A G B P C = A P C + B P C
30 29 imp U CPreHil OLD A X B X C X A G B P C = A P C + B P C