Step |
Hyp |
Ref |
Expression |
1 |
|
choc1 |
|- ( _|_ ` ~H ) = 0H |
2 |
1
|
fveq2i |
|- ( projh ` ( _|_ ` ~H ) ) = ( projh ` 0H ) |
3 |
|
df-h0op |
|- 0hop = ( projh ` 0H ) |
4 |
2 3
|
eqtr4i |
|- ( projh ` ( _|_ ` ~H ) ) = 0hop |
5 |
4
|
fveq1i |
|- ( ( projh ` ( _|_ ` ~H ) ) ` A ) = ( 0hop ` A ) |
6 |
|
helch |
|- ~H e. CH |
7 |
|
pjo |
|- ( ( ~H e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` ~H ) ) ` A ) = ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) ) |
8 |
6 7
|
mpan |
|- ( A e. ~H -> ( ( projh ` ( _|_ ` ~H ) ) ` A ) = ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) ) |
9 |
5 8
|
syl5eqr |
|- ( A e. ~H -> ( 0hop ` A ) = ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) ) |
10 |
6
|
pjhcli |
|- ( A e. ~H -> ( ( projh ` ~H ) ` A ) e. ~H ) |
11 |
|
hvsubid |
|- ( ( ( projh ` ~H ) ` A ) e. ~H -> ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) = 0h ) |
12 |
10 11
|
syl |
|- ( A e. ~H -> ( ( ( projh ` ~H ) ` A ) -h ( ( projh ` ~H ) ` A ) ) = 0h ) |
13 |
9 12
|
eqtrd |
|- ( A e. ~H -> ( 0hop ` A ) = 0h ) |