Step |
Hyp |
Ref |
Expression |
1 |
|
axpjpj |
|- ( ( H e. CH /\ A e. ~H ) -> A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) |
2 |
1
|
eqcomd |
|- ( ( H e. CH /\ A e. ~H ) -> ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = A ) |
3 |
|
simpr |
|- ( ( H e. CH /\ A e. ~H ) -> A e. ~H ) |
4 |
|
pjhcl |
|- ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) e. ~H ) |
5 |
|
choccl |
|- ( H e. CH -> ( _|_ ` H ) e. CH ) |
6 |
|
pjhcl |
|- ( ( ( _|_ ` H ) e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H ) |
7 |
5 6
|
sylan |
|- ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H ) |
8 |
|
hvsubadd |
|- ( ( A e. ~H /\ ( ( projh ` H ) ` A ) e. ~H /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H ) -> ( ( A -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( _|_ ` H ) ) ` A ) <-> ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = A ) ) |
9 |
3 4 7 8
|
syl3anc |
|- ( ( H e. CH /\ A e. ~H ) -> ( ( A -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( _|_ ` H ) ) ` A ) <-> ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = A ) ) |
10 |
2 9
|
mpbird |
|- ( ( H e. CH /\ A e. ~H ) -> ( A -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( _|_ ` H ) ) ` A ) ) |
11 |
10
|
eqcomd |
|- ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) = ( A -h ( ( projh ` H ) ` A ) ) ) |