Step |
Hyp |
Ref |
Expression |
1 |
|
pjoc2.1 |
|- H e. CH |
2 |
|
pjoc2.2 |
|- A e. ~H |
3 |
1
|
choccli |
|- ( _|_ ` H ) e. CH |
4 |
3 2
|
pjoc1i |
|- ( A e. ( _|_ ` H ) <-> ( ( projh ` ( _|_ ` ( _|_ ` H ) ) ) ` A ) = 0h ) |
5 |
1
|
pjococi |
|- ( _|_ ` ( _|_ ` H ) ) = H |
6 |
5
|
fveq2i |
|- ( projh ` ( _|_ ` ( _|_ ` H ) ) ) = ( projh ` H ) |
7 |
6
|
fveq1i |
|- ( ( projh ` ( _|_ ` ( _|_ ` H ) ) ) ` A ) = ( ( projh ` H ) ` A ) |
8 |
7
|
eqeq1i |
|- ( ( ( projh ` ( _|_ ` ( _|_ ` H ) ) ) ` A ) = 0h <-> ( ( projh ` H ) ` A ) = 0h ) |
9 |
4 8
|
bitri |
|- ( A e. ( _|_ ` H ) <-> ( ( projh ` H ) ` A ) = 0h ) |