Metamath Proof Explorer

Theorem ip2dii

Description: Inner product of two sums. (Contributed by NM, 17-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ip2dii.1 
|- X = ( BaseSet ` U )
ip2dii.2 
|- G = ( +v ` U )
ip2dii.7 
|- P = ( .iOLD ` U )
ip2dii.u 
|- U e. CPreHilOLD
ip2dii.a 
|- A e. X
ip2dii.b 
|- B e. X
ip2dii.c 
|- C e. X
ip2dii.d 
|- D e. X
Assertion ip2dii 
|- ( ( A G B ) P ( C G D ) ) = ( ( ( A P C ) + ( B P D ) ) + ( ( A P D ) + ( B P C ) ) )

Proof

Step Hyp Ref Expression
1 ip2dii.1 
 |-  X = ( BaseSet ` U )
2 ip2dii.2 
 |-  G = ( +v ` U )
3 ip2dii.7 
 |-  P = ( .iOLD ` U )
4 ip2dii.u 
 |-  U e. CPreHilOLD
5 ip2dii.a 
 |-  A e. X
6 ip2dii.b 
 |-  B e. X
7 ip2dii.c 
 |-  C e. X
8 ip2dii.d 
 |-  D e. X
9 5 7 8 3pm3.2i 
 |-  ( A e. X /\ C e. X /\ D e. X )
10 1 2 3 dipdi 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ C e. X /\ D e. X ) ) -> ( A P ( C G D ) ) = ( ( A P C ) + ( A P D ) ) )
11 4 9 10 mp2an 
 |-  ( A P ( C G D ) ) = ( ( A P C ) + ( A P D ) )
12 6 7 8 3pm3.2i 
 |-  ( B e. X /\ C e. X /\ D e. X )
13 1 2 3 dipdi 
 |-  ( ( U e. CPreHilOLD /\ ( B e. X /\ C e. X /\ D e. X ) ) -> ( B P ( C G D ) ) = ( ( B P C ) + ( B P D ) ) )
14 4 12 13 mp2an 
 |-  ( B P ( C G D ) ) = ( ( B P C ) + ( B P D ) )
15 11 14 oveq12i 
 |-  ( ( A P ( C G D ) ) + ( B P ( C G D ) ) ) = ( ( ( A P C ) + ( A P D ) ) + ( ( B P C ) + ( B P D ) ) )
16 4 phnvi 
 |-  U e. NrmCVec
17 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ C e. X /\ D e. X ) -> ( C G D ) e. X )
18 16 7 8 17 mp3an 
 |-  ( C G D ) e. X
19 5 6 18 3pm3.2i 
 |-  ( A e. X /\ B e. X /\ ( C G D ) e. X )
20 1 2 3 dipdir 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ ( C G D ) e. X ) ) -> ( ( A G B ) P ( C G D ) ) = ( ( A P ( C G D ) ) + ( B P ( C G D ) ) ) )
21 4 19 20 mp2an 
 |-  ( ( A G B ) P ( C G D ) ) = ( ( A P ( C G D ) ) + ( B P ( C G D ) ) )
22 1 3 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ C e. X ) -> ( A P C ) e. CC )
23 16 5 7 22 mp3an 
 |-  ( A P C ) e. CC
24 1 3 dipcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ D e. X ) -> ( B P D ) e. CC )
25 16 6 8 24 mp3an 
 |-  ( B P D ) e. CC
26 1 3 dipcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ D e. X ) -> ( A P D ) e. CC )
27 16 5 8 26 mp3an 
 |-  ( A P D ) e. CC
28 1 3 dipcl 
 |-  ( ( U e. NrmCVec /\ B e. X /\ C e. X ) -> ( B P C ) e. CC )
29 16 6 7 28 mp3an 
 |-  ( B P C ) e. CC
30 23 25 27 29 add42i 
 |-  ( ( ( A P C ) + ( B P D ) ) + ( ( A P D ) + ( B P C ) ) ) = ( ( ( A P C ) + ( A P D ) ) + ( ( B P C ) + ( B P D ) ) )
31 15 21 30 3eqtr4i 
 |-  ( ( A G B ) P ( C G D ) ) = ( ( ( A P C ) + ( B P D ) ) + ( ( A P D ) + ( B P C ) ) )