This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ip2i

Description: Equation 6.48 of Ponnusamy p. 362. (Contributed by NM, 26-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 
|- X = ( BaseSet ` U )
ip1i.2 
|- G = ( +v ` U )
ip1i.4 
|- S = ( .sOLD ` U )
ip1i.7 
|- P = ( .iOLD ` U )
ip1i.9 
|- U e. CPreHilOLD
ip2i.8 
|- A e. X
ip2i.9 
|- B e. X
Assertion ip2i 
|- ( ( 2 S A ) P B ) = ( 2 x. ( A P B ) )

Proof

Step Hyp Ref Expression
1 ip1i.1 
 |-  X = ( BaseSet ` U )
2 ip1i.2 
 |-  G = ( +v ` U )
3 ip1i.4 
 |-  S = ( .sOLD ` U )
4 ip1i.7 
 |-  P = ( .iOLD ` U )
5 ip1i.9 
 |-  U e. CPreHilOLD
6 ip2i.8 
 |-  A e. X
7 ip2i.9 
 |-  B e. X
8 5 phnvi 
 |-  U e. NrmCVec
9 1 2 nvgcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ A e. X ) -> ( A G A ) e. X )
10 8 6 6 9 mp3an 
 |-  ( A G A ) e. X
11 1 4 dipcl 
 |-  ( ( U e. NrmCVec /\ ( A G A ) e. X /\ B e. X ) -> ( ( A G A ) P B ) e. CC )
12 8 10 7 11 mp3an 
 |-  ( ( A G A ) P B ) e. CC
13 12 addridi 
 |-  ( ( ( A G A ) P B ) + 0 ) = ( ( A G A ) P B )
14 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
15 1 2 3 14 nvrinv 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( A G ( -u 1 S A ) ) = ( 0vec ` U ) )
16 8 6 15 mp2an 
 |-  ( A G ( -u 1 S A ) ) = ( 0vec ` U )
17 16 oveq1i 
 |-  ( ( A G ( -u 1 S A ) ) P B ) = ( ( 0vec ` U ) P B )
18 1 14 4 dip0l 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( ( 0vec ` U ) P B ) = 0 )
19 8 7 18 mp2an 
 |-  ( ( 0vec ` U ) P B ) = 0
20 17 19 eqtri 
 |-  ( ( A G ( -u 1 S A ) ) P B ) = 0
21 20 oveq2i 
 |-  ( ( ( A G A ) P B ) + ( ( A G ( -u 1 S A ) ) P B ) ) = ( ( ( A G A ) P B ) + 0 )
22 df-2 
 |-  2 = ( 1 + 1 )
23 22 oveq1i 
 |-  ( 2 S A ) = ( ( 1 + 1 ) S A )
24 ax-1cn 
 |-  1 e. CC
25 24 24 6 3pm3.2i 
 |-  ( 1 e. CC /\ 1 e. CC /\ A e. X )
26 1 2 3 nvdir 
 |-  ( ( U e. NrmCVec /\ ( 1 e. CC /\ 1 e. CC /\ A e. X ) ) -> ( ( 1 + 1 ) S A ) = ( ( 1 S A ) G ( 1 S A ) ) )
27 8 25 26 mp2an 
 |-  ( ( 1 + 1 ) S A ) = ( ( 1 S A ) G ( 1 S A ) )
28 1 3 nvsid 
 |-  ( ( U e. NrmCVec /\ A e. X ) -> ( 1 S A ) = A )
29 8 6 28 mp2an 
 |-  ( 1 S A ) = A
30 29 29 oveq12i 
 |-  ( ( 1 S A ) G ( 1 S A ) ) = ( A G A )
31 27 30 eqtri 
 |-  ( ( 1 + 1 ) S A ) = ( A G A )
32 23 31 eqtri 
 |-  ( 2 S A ) = ( A G A )
33 32 oveq1i 
 |-  ( ( 2 S A ) P B ) = ( ( A G A ) P B )
34 13 21 33 3eqtr4ri 
 |-  ( ( 2 S A ) P B ) = ( ( ( A G A ) P B ) + ( ( A G ( -u 1 S A ) ) P B ) )
35 1 2 3 4 5 6 6 7 ip1i 
 |-  ( ( ( A G A ) P B ) + ( ( A G ( -u 1 S A ) ) P B ) ) = ( 2 x. ( A P B ) )
36 34 35 eqtri 
 |-  ( ( 2 S A ) P B ) = ( 2 x. ( A P B ) )