This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- H e. CH
pjop.2 
|- A e. ~H
Assertion pjoc1i 
|- ( A e. H <-> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h )

Proof

Step Hyp Ref Expression
1 pjop.1 
 |-  H e. CH
2 pjop.2 
 |-  A e. ~H
3 1 2 pjopi 
 |-  ( ( projh ` ( _|_ ` H ) ) ` A ) = ( A -h ( ( projh ` H ) ` A ) )
4 1 chshii 
 |-  H e. SH
5 1 2 pjclii 
 |-  ( ( projh ` H ) ` A ) e. H
6 shsubcl 
 |-  ( ( H e. SH /\ A e. H /\ ( ( projh ` H ) ` A ) e. H ) -> ( A -h ( ( projh ` H ) ` A ) ) e. H )
7 4 5 6 mp3an13 
 |-  ( A e. H -> ( A -h ( ( projh ` H ) ` A ) ) e. H )
8 3 7 eqeltrid 
 |-  ( A e. H -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. H )
9 1 choccli 
 |-  ( _|_ ` H ) e. CH
10 9 2 pjclii 
 |-  ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H )
11 8 10 jctir 
 |-  ( A e. H -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) e. H /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) ) )
12 elin 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( H i^i ( _|_ ` H ) ) <-> ( ( ( projh ` ( _|_ ` H ) ) ` A ) e. H /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( _|_ ` H ) ) )
13 11 12 sylibr 
 |-  ( A e. H -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. ( H i^i ( _|_ ` H ) ) )
14 ocin 
 |-  ( H e. SH -> ( H i^i ( _|_ ` H ) ) = 0H )
15 4 14 ax-mp 
 |-  ( H i^i ( _|_ ` H ) ) = 0H
16 13 15 eleqtrdi 
 |-  ( A e. H -> ( ( projh ` ( _|_ ` H ) ) ` A ) e. 0H )
17 elch0 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) e. 0H <-> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h )
18 16 17 sylib 
 |-  ( A e. H -> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h )
19 1 2 pjpji 
 |-  A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) )
20 oveq2 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h -> ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) = ( ( ( projh ` H ) ` A ) +h 0h ) )
21 19 20 eqtrid 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h -> A = ( ( ( projh ` H ) ` A ) +h 0h ) )
22 1 2 pjhclii 
 |-  ( ( projh ` H ) ` A ) e. ~H
23 ax-hvaddid 
 |-  ( ( ( projh ` H ) ` A ) e. ~H -> ( ( ( projh ` H ) ` A ) +h 0h ) = ( ( projh ` H ) ` A ) )
24 22 23 ax-mp 
 |-  ( ( ( projh ` H ) ` A ) +h 0h ) = ( ( projh ` H ) ` A )
25 21 24 eqtrdi 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h -> A = ( ( projh ` H ) ` A ) )
26 25 5 eqeltrdi 
 |-  ( ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h -> A e. H )
27 18 26 impbii 
 |-  ( A e. H <-> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h )