Step |
Hyp |
Ref |
Expression |
1 |
|
ajfun.5 |
|- A = ( U adj W ) |
2 |
|
oveq1 |
|- ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( U adj W ) = ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj W ) ) |
3 |
1 2
|
eqtrid |
|- ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> A = ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj W ) ) |
4 |
3
|
funeqd |
|- ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( Fun A <-> Fun ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj W ) ) ) |
5 |
|
oveq2 |
|- ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj W ) = ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ) |
6 |
5
|
funeqd |
|- ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( Fun ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj W ) <-> Fun ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ) ) |
7 |
|
eqid |
|- ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) = ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) |
8 |
|
elimphu |
|- if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) e. CPreHilOLD |
9 |
|
elimnvu |
|- if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) e. NrmCVec |
10 |
7 8 9
|
ajfuni |
|- Fun ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) |
11 |
4 6 10
|
dedth2h |
|- ( ( U e. CPreHilOLD /\ W e. NrmCVec ) -> Fun A ) |