Step |
Hyp |
Ref |
Expression |
1 |
|
pjidm.1 |
⊢ 𝐻 ∈ Cℋ |
2 |
|
pjidm.2 |
⊢ 𝐴 ∈ ℋ |
3 |
|
pjsslem.1 |
⊢ 𝐺 ∈ Cℋ |
4 |
1
|
choccli |
⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ |
5 |
4 2
|
pjclii |
⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) |
6 |
1 3
|
chsscon3i |
⊢ ( 𝐻 ⊆ 𝐺 ↔ ( ⊥ ‘ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) ) |
7 |
3
|
choccli |
⊢ ( ⊥ ‘ 𝐺 ) ∈ Cℋ |
8 |
7 2
|
pjclii |
⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐺 ) |
9 |
|
ssel |
⊢ ( ( ⊥ ‘ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐺 ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) ) |
10 |
8 9
|
mpi |
⊢ ( ( ⊥ ‘ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) |
11 |
6 10
|
sylbi |
⊢ ( 𝐻 ⊆ 𝐺 → ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) |
12 |
4
|
chshii |
⊢ ( ⊥ ‘ 𝐻 ) ∈ Sℋ |
13 |
|
shsubcl |
⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Sℋ ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) |
14 |
12 13
|
mp3an1 |
⊢ ( ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) |
15 |
5 11 14
|
sylancr |
⊢ ( 𝐻 ⊆ 𝐺 → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) |
16 |
1 2 3
|
pjsslem |
⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) |
17 |
16
|
eleq1i |
⊢ ( ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) |
18 |
3 2
|
pjhclii |
⊢ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℋ |
19 |
1 2
|
pjhclii |
⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ |
20 |
18 19
|
hvsubcli |
⊢ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ℋ |
21 |
1 20
|
pjoc2i |
⊢ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ ) |
22 |
17 21
|
bitri |
⊢ ( ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ ) |
23 |
1 18 19
|
pjsubii |
⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) |
24 |
23
|
eqeq1i |
⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ ↔ ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ ) |
25 |
1 18
|
pjhclii |
⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ∈ ℋ |
26 |
1 19
|
pjhclii |
⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ℋ |
27 |
25 26
|
hvsubeq0i |
⊢ ( ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) |
28 |
24 27
|
bitri |
⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) = 0ℎ ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) |
29 |
1 2
|
pjidmi |
⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) |
30 |
29
|
eqeq2i |
⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) |
31 |
22 28 30
|
3bitrri |
⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ↔ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐺 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) |
32 |
15 31
|
sylibr |
⊢ ( 𝐻 ⊆ 𝐺 → ( ( projℎ ‘ 𝐻 ) ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) |