| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pjocin.1 |
|- G e. CH |
| 2 |
|
pjocin.2 |
|- H e. CH |
| 3 |
1 2
|
chincli |
|- ( G i^i H ) e. CH |
| 4 |
3
|
choccli |
|- ( _|_ ` ( G i^i H ) ) e. CH |
| 5 |
4
|
cheli |
|- ( A e. ( _|_ ` ( G i^i H ) ) -> A e. ~H ) |
| 6 |
|
pjpo |
|- ( ( G e. CH /\ A e. ~H ) -> ( ( projh ` G ) ` A ) = ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) ) |
| 7 |
1 5 6
|
sylancr |
|- ( A e. ( _|_ ` ( G i^i H ) ) -> ( ( projh ` G ) ` A ) = ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) ) |
| 8 |
|
inss1 |
|- ( G i^i H ) C_ G |
| 9 |
3 1
|
chsscon3i |
|- ( ( G i^i H ) C_ G <-> ( _|_ ` G ) C_ ( _|_ ` ( G i^i H ) ) ) |
| 10 |
8 9
|
mpbi |
|- ( _|_ ` G ) C_ ( _|_ ` ( G i^i H ) ) |
| 11 |
1
|
choccli |
|- ( _|_ ` G ) e. CH |
| 12 |
11
|
pjcli |
|- ( A e. ~H -> ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` G ) ) |
| 13 |
5 12
|
syl |
|- ( A e. ( _|_ ` ( G i^i H ) ) -> ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` G ) ) |
| 14 |
10 13
|
sselid |
|- ( A e. ( _|_ ` ( G i^i H ) ) -> ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` ( G i^i H ) ) ) |
| 15 |
4
|
chshii |
|- ( _|_ ` ( G i^i H ) ) e. SH |
| 16 |
|
shsubcl |
|- ( ( ( _|_ ` ( G i^i H ) ) e. SH /\ A e. ( _|_ ` ( G i^i H ) ) /\ ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` ( G i^i H ) ) ) -> ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` ( G i^i H ) ) ) |
| 17 |
15 16
|
mp3an1 |
|- ( ( A e. ( _|_ ` ( G i^i H ) ) /\ ( ( projh ` ( _|_ ` G ) ) ` A ) e. ( _|_ ` ( G i^i H ) ) ) -> ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` ( G i^i H ) ) ) |
| 18 |
14 17
|
mpdan |
|- ( A e. ( _|_ ` ( G i^i H ) ) -> ( A -h ( ( projh ` ( _|_ ` G ) ) ` A ) ) e. ( _|_ ` ( G i^i H ) ) ) |
| 19 |
7 18
|
eqeltrd |
|- ( A e. ( _|_ ` ( G i^i H ) ) -> ( ( projh ` G ) ` A ) e. ( _|_ ` ( G i^i H ) ) ) |