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 |
|
oveq1 |
|- ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( A G B ) = ( if ( A e. X , A , ( 0vec ` U ) ) G B ) ) |
7 |
6
|
oveq1d |
|- ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( ( A G B ) P C ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) G B ) P C ) ) |
8 |
|
oveq1 |
|- ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( A P C ) = ( if ( A e. X , A , ( 0vec ` U ) ) P C ) ) |
9 |
8
|
oveq1d |
|- ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( ( A P C ) + ( B P C ) ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) P C ) + ( B P C ) ) ) |
10 |
7 9
|
eqeq12d |
|- ( A = if ( A e. X , A , ( 0vec ` U ) ) -> ( ( ( A G B ) P C ) = ( ( A P C ) + ( B P C ) ) <-> ( ( if ( A e. X , A , ( 0vec ` U ) ) G B ) P C ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) P C ) + ( B P C ) ) ) ) |
11 |
|
oveq2 |
|- ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( if ( A e. X , A , ( 0vec ` U ) ) G B ) = ( if ( A e. X , A , ( 0vec ` U ) ) G if ( B e. X , B , ( 0vec ` U ) ) ) ) |
12 |
11
|
oveq1d |
|- ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( ( if ( A e. X , A , ( 0vec ` U ) ) G B ) P C ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) G if ( B e. X , B , ( 0vec ` U ) ) ) P C ) ) |
13 |
|
oveq1 |
|- ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( B P C ) = ( if ( B e. X , B , ( 0vec ` U ) ) P C ) ) |
14 |
13
|
oveq2d |
|- ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( ( if ( A e. X , A , ( 0vec ` U ) ) P C ) + ( B P C ) ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) P C ) + ( if ( B e. X , B , ( 0vec ` U ) ) P C ) ) ) |
15 |
12 14
|
eqeq12d |
|- ( B = if ( B e. X , B , ( 0vec ` U ) ) -> ( ( ( if ( A e. X , A , ( 0vec ` U ) ) G B ) P C ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) P C ) + ( B P C ) ) <-> ( ( if ( A e. X , A , ( 0vec ` U ) ) G if ( B e. X , B , ( 0vec ` U ) ) ) P C ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) P C ) + ( if ( B e. X , B , ( 0vec ` U ) ) P C ) ) ) ) |
16 |
|
oveq2 |
|- ( C = if ( C e. X , C , ( 0vec ` U ) ) -> ( ( if ( A e. X , A , ( 0vec ` U ) ) G if ( B e. X , B , ( 0vec ` U ) ) ) P C ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) G if ( B e. X , B , ( 0vec ` U ) ) ) P if ( C e. X , C , ( 0vec ` U ) ) ) ) |
17 |
|
oveq2 |
|- ( C = if ( C e. X , C , ( 0vec ` U ) ) -> ( if ( A e. X , A , ( 0vec ` U ) ) P C ) = ( if ( A e. X , A , ( 0vec ` U ) ) P if ( C e. X , C , ( 0vec ` U ) ) ) ) |
18 |
|
oveq2 |
|- ( C = if ( C e. X , C , ( 0vec ` U ) ) -> ( if ( B e. X , B , ( 0vec ` U ) ) P C ) = ( if ( B e. X , B , ( 0vec ` U ) ) P if ( C e. X , C , ( 0vec ` U ) ) ) ) |
19 |
17 18
|
oveq12d |
|- ( C = if ( C e. X , C , ( 0vec ` U ) ) -> ( ( if ( A e. X , A , ( 0vec ` U ) ) P C ) + ( if ( B e. X , B , ( 0vec ` U ) ) P C ) ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) P if ( C e. X , C , ( 0vec ` U ) ) ) + ( if ( B e. X , B , ( 0vec ` U ) ) P if ( C e. X , C , ( 0vec ` U ) ) ) ) ) |
20 |
16 19
|
eqeq12d |
|- ( C = if ( C e. X , C , ( 0vec ` U ) ) -> ( ( ( if ( A e. X , A , ( 0vec ` U ) ) G if ( B e. X , B , ( 0vec ` U ) ) ) P C ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) P C ) + ( if ( B e. X , B , ( 0vec ` U ) ) P C ) ) <-> ( ( if ( A e. X , A , ( 0vec ` U ) ) G if ( B e. X , B , ( 0vec ` U ) ) ) P if ( C e. X , C , ( 0vec ` U ) ) ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) P if ( C e. X , C , ( 0vec ` U ) ) ) + ( if ( B e. X , B , ( 0vec ` U ) ) P if ( C e. X , C , ( 0vec ` U ) ) ) ) ) ) |
21 |
|
eqid |
|- ( 0vec ` U ) = ( 0vec ` U ) |
22 |
1 21 5
|
elimph |
|- if ( A e. X , A , ( 0vec ` U ) ) e. X |
23 |
1 21 5
|
elimph |
|- if ( B e. X , B , ( 0vec ` U ) ) e. X |
24 |
1 21 5
|
elimph |
|- if ( C e. X , C , ( 0vec ` U ) ) e. X |
25 |
1 2 3 4 5 22 23 24
|
ipdirilem |
|- ( ( if ( A e. X , A , ( 0vec ` U ) ) G if ( B e. X , B , ( 0vec ` U ) ) ) P if ( C e. X , C , ( 0vec ` U ) ) ) = ( ( if ( A e. X , A , ( 0vec ` U ) ) P if ( C e. X , C , ( 0vec ` U ) ) ) + ( if ( B e. X , B , ( 0vec ` U ) ) P if ( C e. X , C , ( 0vec ` U ) ) ) ) |
26 |
10 15 20 25
|
dedth3h |
|- ( ( A e. X /\ B e. X /\ C e. X ) -> ( ( A G B ) P C ) = ( ( A P C ) + ( B P C ) ) ) |