Metamath Proof Explorer


Theorem pjoi0

Description: The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion pjoi0 ( ( ( 𝐺C𝐻C𝐴 ∈ ℋ ) ∧ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) → ( ( ( proj𝐺 ) ‘ 𝐴 ) ·ih ( ( proj𝐻 ) ‘ 𝐴 ) ) = 0 )

Proof

Step Hyp Ref Expression
1 pjrn ( 𝐺C → ran ( proj𝐺 ) = 𝐺 )
2 1 adantr ( ( 𝐺C𝐻C ) → ran ( proj𝐺 ) = 𝐺 )
3 pjrn ( 𝐻C → ran ( proj𝐻 ) = 𝐻 )
4 3 fveq2d ( 𝐻C → ( ⊥ ‘ ran ( proj𝐻 ) ) = ( ⊥ ‘ 𝐻 ) )
5 4 adantl ( ( 𝐺C𝐻C ) → ( ⊥ ‘ ran ( proj𝐻 ) ) = ( ⊥ ‘ 𝐻 ) )
6 2 5 sseq12d ( ( 𝐺C𝐻C ) → ( ran ( proj𝐺 ) ⊆ ( ⊥ ‘ ran ( proj𝐻 ) ) ↔ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) )
7 6 biimpar ( ( ( 𝐺C𝐻C ) ∧ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) → ran ( proj𝐺 ) ⊆ ( ⊥ ‘ ran ( proj𝐻 ) ) )
8 7 3adantl3 ( ( ( 𝐺C𝐻C𝐴 ∈ ℋ ) ∧ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) → ran ( proj𝐺 ) ⊆ ( ⊥ ‘ ran ( proj𝐻 ) ) )
9 id ( 𝐻C𝐻C )
10 3 9 eqeltrd ( 𝐻C → ran ( proj𝐻 ) ∈ C )
11 chsh ( ran ( proj𝐻 ) ∈ C → ran ( proj𝐻 ) ∈ S )
12 10 11 syl ( 𝐻C → ran ( proj𝐻 ) ∈ S )
13 12 3ad2ant2 ( ( 𝐺C𝐻C𝐴 ∈ ℋ ) → ran ( proj𝐻 ) ∈ S )
14 13 adantr ( ( ( 𝐺C𝐻C𝐴 ∈ ℋ ) ∧ ran ( proj𝐺 ) ⊆ ( ⊥ ‘ ran ( proj𝐻 ) ) ) → ran ( proj𝐻 ) ∈ S )
15 simpr ( ( ( 𝐺C𝐻C𝐴 ∈ ℋ ) ∧ ran ( proj𝐺 ) ⊆ ( ⊥ ‘ ran ( proj𝐻 ) ) ) → ran ( proj𝐺 ) ⊆ ( ⊥ ‘ ran ( proj𝐻 ) ) )
16 pjfn ( 𝐺C → ( proj𝐺 ) Fn ℋ )
17 fnfvelrn ( ( ( proj𝐺 ) Fn ℋ ∧ 𝐴 ∈ ℋ ) → ( ( proj𝐺 ) ‘ 𝐴 ) ∈ ran ( proj𝐺 ) )
18 16 17 sylan ( ( 𝐺C𝐴 ∈ ℋ ) → ( ( proj𝐺 ) ‘ 𝐴 ) ∈ ran ( proj𝐺 ) )
19 18 3adant2 ( ( 𝐺C𝐻C𝐴 ∈ ℋ ) → ( ( proj𝐺 ) ‘ 𝐴 ) ∈ ran ( proj𝐺 ) )
20 pjfn ( 𝐻C → ( proj𝐻 ) Fn ℋ )
21 fnfvelrn ( ( ( proj𝐻 ) Fn ℋ ∧ 𝐴 ∈ ℋ ) → ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ran ( proj𝐻 ) )
22 20 21 sylan ( ( 𝐻C𝐴 ∈ ℋ ) → ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ran ( proj𝐻 ) )
23 22 3adant1 ( ( 𝐺C𝐻C𝐴 ∈ ℋ ) → ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ran ( proj𝐻 ) )
24 19 23 jca ( ( 𝐺C𝐻C𝐴 ∈ ℋ ) → ( ( ( proj𝐺 ) ‘ 𝐴 ) ∈ ran ( proj𝐺 ) ∧ ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ran ( proj𝐻 ) ) )
25 24 adantr ( ( ( 𝐺C𝐻C𝐴 ∈ ℋ ) ∧ ran ( proj𝐺 ) ⊆ ( ⊥ ‘ ran ( proj𝐻 ) ) ) → ( ( ( proj𝐺 ) ‘ 𝐴 ) ∈ ran ( proj𝐺 ) ∧ ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ran ( proj𝐻 ) ) )
26 shorth ( ran ( proj𝐻 ) ∈ S → ( ran ( proj𝐺 ) ⊆ ( ⊥ ‘ ran ( proj𝐻 ) ) → ( ( ( ( proj𝐺 ) ‘ 𝐴 ) ∈ ran ( proj𝐺 ) ∧ ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ran ( proj𝐻 ) ) → ( ( ( proj𝐺 ) ‘ 𝐴 ) ·ih ( ( proj𝐻 ) ‘ 𝐴 ) ) = 0 ) ) )
27 14 15 25 26 syl3c ( ( ( 𝐺C𝐻C𝐴 ∈ ℋ ) ∧ ran ( proj𝐺 ) ⊆ ( ⊥ ‘ ran ( proj𝐻 ) ) ) → ( ( ( proj𝐺 ) ‘ 𝐴 ) ·ih ( ( proj𝐻 ) ‘ 𝐴 ) ) = 0 )
28 8 27 syldan ( ( ( 𝐺C𝐻C𝐴 ∈ ℋ ) ∧ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) → ( ( ( proj𝐺 ) ‘ 𝐴 ) ·ih ( ( proj𝐻 ) ‘ 𝐴 ) ) = 0 )