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 )