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