Step |
Hyp |
Ref |
Expression |
1 |
|
pjidm.1 |
|- H e. CH |
2 |
|
pjidm.2 |
|- A e. ~H |
3 |
|
pjadj.3 |
|- B e. ~H |
4 |
3 2
|
pjorthi |
|- ( H e. CH -> ( ( ( projh ` H ) ` B ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) = 0 ) |
5 |
1 4
|
ax-mp |
|- ( ( ( projh ` H ) ` B ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) = 0 |
6 |
5
|
fveq2i |
|- ( * ` ( ( ( projh ` H ) ` B ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) = ( * ` 0 ) |
7 |
|
cj0 |
|- ( * ` 0 ) = 0 |
8 |
6 7
|
eqtri |
|- ( * ` ( ( ( projh ` H ) ` B ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) = 0 |
9 |
1
|
choccli |
|- ( _|_ ` H ) e. CH |
10 |
9 2
|
pjhclii |
|- ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H |
11 |
1 3
|
pjhclii |
|- ( ( projh ` H ) ` B ) e. ~H |
12 |
10 11
|
his1i |
|- ( ( ( projh ` ( _|_ ` H ) ) ` A ) .ih ( ( projh ` H ) ` B ) ) = ( * ` ( ( ( projh ` H ) ` B ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) |
13 |
2 3
|
pjorthi |
|- ( H e. CH -> ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) = 0 ) |
14 |
1 13
|
ax-mp |
|- ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) = 0 |
15 |
8 12 14
|
3eqtr4ri |
|- ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) = ( ( ( projh ` ( _|_ ` H ) ) ` A ) .ih ( ( projh ` H ) ` B ) ) |
16 |
15
|
oveq2i |
|- ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) = ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` ( _|_ ` H ) ) ` A ) .ih ( ( projh ` H ) ` B ) ) ) |
17 |
1 2
|
pjhclii |
|- ( ( projh ` H ) ` A ) e. ~H |
18 |
9 3
|
pjhclii |
|- ( ( projh ` ( _|_ ` H ) ) ` B ) e. ~H |
19 |
|
his7 |
|- ( ( ( ( projh ` H ) ` A ) e. ~H /\ ( ( projh ` H ) ` B ) e. ~H /\ ( ( projh ` ( _|_ ` H ) ) ` B ) e. ~H ) -> ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) = ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) ) |
20 |
17 11 18 19
|
mp3an |
|- ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) = ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) |
21 |
|
ax-his2 |
|- ( ( ( ( projh ` H ) ` A ) e. ~H /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H /\ ( ( projh ` H ) ` B ) e. ~H ) -> ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) .ih ( ( projh ` H ) ` B ) ) = ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` ( _|_ ` H ) ) ` A ) .ih ( ( projh ` H ) ` B ) ) ) ) |
22 |
17 10 11 21
|
mp3an |
|- ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) .ih ( ( projh ` H ) ` B ) ) = ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` H ) ` B ) ) + ( ( ( projh ` ( _|_ ` H ) ) ` A ) .ih ( ( projh ` H ) ` B ) ) ) |
23 |
16 20 22
|
3eqtr4i |
|- ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) = ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) .ih ( ( projh ` H ) ` B ) ) |
24 |
1 3
|
pjpji |
|- B = ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) |
25 |
24
|
oveq2i |
|- ( ( ( projh ` H ) ` A ) .ih B ) = ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` H ) ` B ) +h ( ( projh ` ( _|_ ` H ) ) ` B ) ) ) |
26 |
1 2
|
pjpji |
|- A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) |
27 |
26
|
oveq1i |
|- ( A .ih ( ( projh ` H ) ` B ) ) = ( ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) .ih ( ( projh ` H ) ` B ) ) |
28 |
23 25 27
|
3eqtr4i |
|- ( ( ( projh ` H ) ` A ) .ih B ) = ( A .ih ( ( projh ` H ) ` B ) ) |