Step |
Hyp |
Ref |
Expression |
1 |
|
pjop.1 |
⊢ 𝐻 ∈ Cℋ |
2 |
|
pjop.2 |
⊢ 𝐴 ∈ ℋ |
3 |
1 2
|
pjopi |
⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = ( 𝐴 −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) |
4 |
1
|
chshii |
⊢ 𝐻 ∈ Sℋ |
5 |
1 2
|
pjclii |
⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 |
6 |
|
shsubcl |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 ) → ( 𝐴 −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ 𝐻 ) |
7 |
4 5 6
|
mp3an13 |
⊢ ( 𝐴 ∈ 𝐻 → ( 𝐴 −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ 𝐻 ) |
8 |
3 7
|
eqeltrid |
⊢ ( 𝐴 ∈ 𝐻 → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ 𝐻 ) |
9 |
1
|
choccli |
⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ |
10 |
9 2
|
pjclii |
⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) |
11 |
8 10
|
jctir |
⊢ ( 𝐴 ∈ 𝐻 → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ 𝐻 ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) ) |
12 |
|
elin |
⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) ↔ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ 𝐻 ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) ) |
13 |
11 12
|
sylibr |
⊢ ( 𝐴 ∈ 𝐻 → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) ) |
14 |
|
ocin |
⊢ ( 𝐻 ∈ Sℋ → ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ ) |
15 |
4 14
|
ax-mp |
⊢ ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ |
16 |
13 15
|
eleqtrdi |
⊢ ( 𝐴 ∈ 𝐻 → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ 0ℋ ) |
17 |
|
elch0 |
⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ 0ℋ ↔ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ ) |
18 |
16 17
|
sylib |
⊢ ( 𝐴 ∈ 𝐻 → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ ) |
19 |
1 2
|
pjpji |
⊢ 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) |
20 |
|
oveq2 |
⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ 0ℎ ) ) |
21 |
19 20
|
syl5eq |
⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ → 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ 0ℎ ) ) |
22 |
1 2
|
pjhclii |
⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ |
23 |
|
ax-hvaddid |
⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ 0ℎ ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) |
24 |
22 23
|
ax-mp |
⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ 0ℎ ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) |
25 |
21 24
|
eqtrdi |
⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ → 𝐴 = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) |
26 |
25 5
|
eqeltrdi |
⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ → 𝐴 ∈ 𝐻 ) |
27 |
18 26
|
impbii |
⊢ ( 𝐴 ∈ 𝐻 ↔ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ ) |