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 )