Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
|- ( H = if ( H e. CH , H , 0H ) -> ( _|_ ` H ) = ( _|_ ` if ( H e. CH , H , 0H ) ) ) |
2 |
1
|
eleq2d |
|- ( H = if ( H e. CH , H , 0H ) -> ( A e. ( _|_ ` H ) <-> A e. ( _|_ ` if ( H e. CH , H , 0H ) ) ) ) |
3 |
|
fveq2 |
|- ( H = if ( H e. CH , H , 0H ) -> ( projh ` H ) = ( projh ` if ( H e. CH , H , 0H ) ) ) |
4 |
3
|
fveq1d |
|- ( H = if ( H e. CH , H , 0H ) -> ( ( projh ` H ) ` A ) = ( ( projh ` if ( H e. CH , H , 0H ) ) ` A ) ) |
5 |
4
|
eqeq1d |
|- ( H = if ( H e. CH , H , 0H ) -> ( ( ( projh ` H ) ` A ) = 0h <-> ( ( projh ` if ( H e. CH , H , 0H ) ) ` A ) = 0h ) ) |
6 |
2 5
|
bibi12d |
|- ( H = if ( H e. CH , H , 0H ) -> ( ( A e. ( _|_ ` H ) <-> ( ( projh ` H ) ` A ) = 0h ) <-> ( A e. ( _|_ ` if ( H e. CH , H , 0H ) ) <-> ( ( projh ` if ( H e. CH , H , 0H ) ) ` A ) = 0h ) ) ) |
7 |
|
eleq1 |
|- ( A = if ( A e. ~H , A , 0h ) -> ( A e. ( _|_ ` if ( H e. CH , H , 0H ) ) <-> if ( A e. ~H , A , 0h ) e. ( _|_ ` if ( H e. CH , H , 0H ) ) ) ) |
8 |
|
fveqeq2 |
|- ( A = if ( A e. ~H , A , 0h ) -> ( ( ( projh ` if ( H e. CH , H , 0H ) ) ` A ) = 0h <-> ( ( projh ` if ( H e. CH , H , 0H ) ) ` if ( A e. ~H , A , 0h ) ) = 0h ) ) |
9 |
7 8
|
bibi12d |
|- ( A = if ( A e. ~H , A , 0h ) -> ( ( A e. ( _|_ ` if ( H e. CH , H , 0H ) ) <-> ( ( projh ` if ( H e. CH , H , 0H ) ) ` A ) = 0h ) <-> ( if ( A e. ~H , A , 0h ) e. ( _|_ ` if ( H e. CH , H , 0H ) ) <-> ( ( projh ` if ( H e. CH , H , 0H ) ) ` if ( A e. ~H , A , 0h ) ) = 0h ) ) ) |
10 |
|
h0elch |
|- 0H e. CH |
11 |
10
|
elimel |
|- if ( H e. CH , H , 0H ) e. CH |
12 |
|
ifhvhv0 |
|- if ( A e. ~H , A , 0h ) e. ~H |
13 |
11 12
|
pjoc2i |
|- ( if ( A e. ~H , A , 0h ) e. ( _|_ ` if ( H e. CH , H , 0H ) ) <-> ( ( projh ` if ( H e. CH , H , 0H ) ) ` if ( A e. ~H , A , 0h ) ) = 0h ) |
14 |
6 9 13
|
dedth2h |
|- ( ( H e. CH /\ A e. ~H ) -> ( A e. ( _|_ ` H ) <-> ( ( projh ` H ) ` A ) = 0h ) ) |