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

Metamath Proof Explorer

Theorem pjdsi

Description: Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 21-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjsumt.1 ⊢ G ∈ C ℋ
pjsumt.2 ⊢ H ∈ C ℋ
Assertion pjdsi ⊢ A ∈ G ∨ ℋ H ∧ G ⊆ ⊥ ⁡ H → A = proj ℎ ⁡ G ⁡ A + ℎ proj ℎ ⁡ H ⁡ A

Proof

Step Hyp Ref Expression
1 pjsumt.1 ⊢ G ∈ C ℋ
2 pjsumt.2 ⊢ H ∈ C ℋ
3 1 2 osumi ⊢ G ⊆ ⊥ ⁡ H → G + ℋ H = G ∨ ℋ H
4 3 fveq2d ⊢ G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H = proj ℎ ⁡ G ∨ ℋ H
5 4 fveq1d ⊢ G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H ⁡ A = proj ℎ ⁡ G ∨ ℋ H ⁡ A
6 1 2 chjcli ⊢ G ∨ ℋ H ∈ C ℋ
7 pjid ⊢ G ∨ ℋ H ∈ C ℋ ∧ A ∈ G ∨ ℋ H → proj ℎ ⁡ G ∨ ℋ H ⁡ A = A
8 6 7 mpan ⊢ A ∈ G ∨ ℋ H → proj ℎ ⁡ G ∨ ℋ H ⁡ A = A
9 5 8 sylan9eqr ⊢ A ∈ G ∨ ℋ H ∧ G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H ⁡ A = A
10 6 cheli ⊢ A ∈ G ∨ ℋ H → A ∈ ℋ
11 1 2 pjsumi ⊢ A ∈ ℋ → G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H ⁡ A = proj ℎ ⁡ G ⁡ A + ℎ proj ℎ ⁡ H ⁡ A
12 11 imp ⊢ A ∈ ℋ ∧ G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H ⁡ A = proj ℎ ⁡ G ⁡ A + ℎ proj ℎ ⁡ H ⁡ A
13 10 12 sylan ⊢ A ∈ G ∨ ℋ H ∧ G ⊆ ⊥ ⁡ H → proj ℎ ⁡ G + ℋ H ⁡ A = proj ℎ ⁡ G ⁡ A + ℎ proj ℎ ⁡ H ⁡ A
14 9 13 eqtr3d ⊢ A ∈ G ∨ ℋ H ∧ G ⊆ ⊥ ⁡ H → A = proj ℎ ⁡ G ⁡ A + ℎ proj ℎ ⁡ H ⁡ A