Step |
Hyp |
Ref |
Expression |
1 |
|
pjidm.1 |
|- H e. CH |
2 |
|
pjidm.2 |
|- A e. ~H |
3 |
|
pjsub.3 |
|- B e. ~H |
4 |
|
neg1cn |
|- -u 1 e. CC |
5 |
4 3
|
hvmulcli |
|- ( -u 1 .h B ) e. ~H |
6 |
1 2 5
|
pjaddii |
|- ( ( projh ` H ) ` ( A +h ( -u 1 .h B ) ) ) = ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` ( -u 1 .h B ) ) ) |
7 |
1 3 4
|
pjmulii |
|- ( ( projh ` H ) ` ( -u 1 .h B ) ) = ( -u 1 .h ( ( projh ` H ) ` B ) ) |
8 |
7
|
oveq2i |
|- ( ( ( projh ` H ) ` A ) +h ( ( projh ` H ) ` ( -u 1 .h B ) ) ) = ( ( ( projh ` H ) ` A ) +h ( -u 1 .h ( ( projh ` H ) ` B ) ) ) |
9 |
6 8
|
eqtri |
|- ( ( projh ` H ) ` ( A +h ( -u 1 .h B ) ) ) = ( ( ( projh ` H ) ` A ) +h ( -u 1 .h ( ( projh ` H ) ` B ) ) ) |
10 |
2 3
|
hvsubvali |
|- ( A -h B ) = ( A +h ( -u 1 .h B ) ) |
11 |
10
|
fveq2i |
|- ( ( projh ` H ) ` ( A -h B ) ) = ( ( projh ` H ) ` ( A +h ( -u 1 .h B ) ) ) |
12 |
1 2
|
pjhclii |
|- ( ( projh ` H ) ` A ) e. ~H |
13 |
1 3
|
pjhclii |
|- ( ( projh ` H ) ` B ) e. ~H |
14 |
12 13
|
hvsubvali |
|- ( ( ( projh ` H ) ` A ) -h ( ( projh ` H ) ` B ) ) = ( ( ( projh ` H ) ` A ) +h ( -u 1 .h ( ( projh ` H ) ` B ) ) ) |
15 |
9 11 14
|
3eqtr4i |
|- ( ( projh ` H ) ` ( A -h B ) ) = ( ( ( projh ` H ) ` A ) -h ( ( projh ` H ) ` B ) ) |