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

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 = ( .iOLD ` U )
Assertion dipdir 
|- ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. 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 = ( .iOLD ` U )
4 fveq2 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( BaseSet ` U ) = ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) )
5 1 4 eqtrid 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> X = ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) )
6 5 eleq2d 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( A e. X <-> A e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) ) )
7 5 eleq2d 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( B e. X <-> B e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) ) )
8 5 eleq2d 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( C e. X <-> C e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) ) )
9 6 7 8 3anbi123d 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( ( A e. X /\ B e. X /\ C e. X ) <-> ( A e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ B e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ C e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) ) ) )
10 fveq2 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( +v ` U ) = ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) )
11 2 10 eqtrid 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> G = ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) )
12 11 oveqd 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( A G B ) = ( A ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) B ) )
13 12 oveq1d 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( ( A G B ) P C ) = ( ( A ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) B ) P C ) )
14 fveq2 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( .iOLD ` U ) = ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) )
15 3 14 eqtrid 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> P = ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) )
16 15 oveqd 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( ( A ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) B ) P C ) = ( ( A ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) B ) ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) )
17 13 16 eqtrd 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( ( A G B ) P C ) = ( ( A ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) B ) ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) )
18 15 oveqd 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( A P C ) = ( A ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) )
19 15 oveqd 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( B P C ) = ( B ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) )
20 18 19 oveq12d 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( ( A P C ) + ( B P C ) ) = ( ( A ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) + ( B ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) ) )
21 17 20 eqeq12d 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( ( ( A G B ) P C ) = ( ( A P C ) + ( B P C ) ) <-> ( ( A ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) B ) ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) = ( ( A ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) + ( B ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) ) ) )
22 9 21 imbi12d 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( ( ( A e. X /\ B e. X /\ C e. X ) -> ( ( A G B ) P C ) = ( ( A P C ) + ( B P C ) ) ) <-> ( ( A e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ B e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ C e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) ) -> ( ( A ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) B ) ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) = ( ( A ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) + ( B ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) ) ) ) )
23 eqid 
 |-  ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) = ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) )
24 eqid 
 |-  ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) = ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) )
25 eqid 
 |-  ( .sOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) = ( .sOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) )
26 eqid 
 |-  ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) = ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) )
27 elimphu 
 |-  if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) e. CPreHilOLD
28 23 24 25 26 27 ipdiri 
 |-  ( ( A e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ B e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) /\ C e. ( BaseSet ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) ) -> ( ( A ( +v ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) B ) ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) = ( ( A ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) + ( B ( .iOLD ` if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) ) C ) ) )
29 22 28 dedth 
 |-  ( U e. CPreHilOLD -> ( ( A e. X /\ B e. X /\ C e. X ) -> ( ( A G B ) P C ) = ( ( A P C ) + ( B P C ) ) ) )
30 29 imp 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) P C ) = ( ( A P C ) + ( B P C ) ) )