Step |
Hyp |
Ref |
Expression |
1 |
|
choccl |
⊢ ( 𝐻 ∈ Cℋ → ( ⊥ ‘ 𝐻 ) ∈ Cℋ ) |
2 |
|
pjhcl |
⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ℋ ) |
3 |
1 2
|
sylan |
⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ℋ ) |
4 |
|
pjhcl |
⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ ) |
5 |
|
ax-hvcom |
⊢ ( ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) |
6 |
3 4 5
|
syl2anc |
⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) |
7 |
|
axpjpj |
⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) |
8 |
6 7
|
eqtr4d |
⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = 𝐴 ) |
9 |
|
simpr |
⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → 𝐴 ∈ ℋ ) |
10 |
|
hvsubadd |
⊢ ( ( 𝐴 ∈ ℋ ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ ) → ( ( 𝐴 −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ↔ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = 𝐴 ) ) |
11 |
9 3 4 10
|
syl3anc |
⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝐴 −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ↔ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = 𝐴 ) ) |
12 |
8 11
|
mpbird |
⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) |
13 |
12
|
eqcomd |
⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = ( 𝐴 −ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) |