Metamath Proof Explorer


Theorem dipdi

Description: Distributive law for inner product. (Contributed by NM, 20-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses dipdir.1 X = BaseSet U
dipdir.2 G = + v U
dipdir.7 P = 𝑖OLD U
Assertion dipdi U CPreHil OLD A X B X C X A P B G C = A P B + A 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 id C X B X A X C X B X A X
5 4 3com13 A X B X C X C X B X A X
6 id B X C X A X B X C X A X
7 6 3com12 C X B X A X B X C X A X
8 1 2 3 dipdir U CPreHil OLD B X C X A X B G C P A = B P A + C P A
9 7 8 sylan2 U CPreHil OLD C X B X A X B G C P A = B P A + C P A
10 9 fveq2d U CPreHil OLD C X B X A X B G C P A = B P A + C P A
11 phnv U CPreHil OLD U NrmCVec
12 simpl U NrmCVec C X B X A X U NrmCVec
13 1 2 nvgcl U NrmCVec B X C X B G C X
14 13 3com23 U NrmCVec C X B X B G C X
15 14 3adant3r3 U NrmCVec C X B X A X B G C X
16 simpr3 U NrmCVec C X B X A X A X
17 1 3 dipcj U NrmCVec B G C X A X B G C P A = A P B G C
18 12 15 16 17 syl3anc U NrmCVec C X B X A X B G C P A = A P B G C
19 11 18 sylan U CPreHil OLD C X B X A X B G C P A = A P B G C
20 1 3 dipcl U NrmCVec B X A X B P A
21 20 3adant3r1 U NrmCVec C X B X A X B P A
22 1 3 dipcl U NrmCVec C X A X C P A
23 22 3adant3r2 U NrmCVec C X B X A X C P A
24 21 23 cjaddd U NrmCVec C X B X A X B P A + C P A = B P A + C P A
25 1 3 dipcj U NrmCVec B X A X B P A = A P B
26 25 3adant3r1 U NrmCVec C X B X A X B P A = A P B
27 1 3 dipcj U NrmCVec C X A X C P A = A P C
28 27 3adant3r2 U NrmCVec C X B X A X C P A = A P C
29 26 28 oveq12d U NrmCVec C X B X A X B P A + C P A = A P B + A P C
30 24 29 eqtrd U NrmCVec C X B X A X B P A + C P A = A P B + A P C
31 11 30 sylan U CPreHil OLD C X B X A X B P A + C P A = A P B + A P C
32 10 19 31 3eqtr3d U CPreHil OLD C X B X A X A P B G C = A P B + A P C
33 5 32 sylan2 U CPreHil OLD A X B X C X A P B G C = A P B + A P C