Metamath Proof Explorer

Theorem pjoc1i

Description: Projection of a vector in the orthocomplement of the projection subspace. (Contributed by NM, 27-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjop.1 ⊢ 𝐻 ∈ Cℋ
pjop.2 ⊢ 𝐴 ∈ ℋ
Assertion pjoc1i ( 𝐴 ∈ 𝐻 ↔ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = 0ℎ )

Proof

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ℎ )