Metamath Proof Explorer

Theorem pjds3i

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

Ref Expression
Hypotheses pjds3.1 ⊢ 𝐹 ∈ Cℋ
pjds3.2 ⊢ 𝐺 ∈ Cℋ
pjds3.3 ⊢ 𝐻 ∈ Cℋ
Assertion pjds3i ( ( ( 𝐴 ∈ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) ∧ 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) ) ∧ ( 𝐹 ⊆ ( ⊥ ‘ 𝐻 ) ∧ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) ) → 𝐴 = ( ( ( ( projℎ ‘ 𝐹 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 pjds3.1 ⊢ 𝐹 ∈ Cℋ
2 pjds3.2 ⊢ 𝐺 ∈ Cℋ
3 pjds3.3 ⊢ 𝐻 ∈ Cℋ
4 simpl ⊢ ( ( 𝐴 ∈ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) ∧ 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) ) → 𝐴 ∈ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) )
5 3 choccli ⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
6 1 2 5 chlubii ⊢ ( ( 𝐹 ⊆ ( ⊥ ‘ 𝐻 ) ∧ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) → ( 𝐹 ∨ℋ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) )
7 1 2 chjcli ⊢ ( 𝐹 ∨ℋ 𝐺 ) ∈ Cℋ
8 7 3 pjdsi ⊢ ( ( 𝐴 ∈ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) ∧ ( 𝐹 ∨ℋ 𝐺 ) ⊆ ( ⊥ ‘ 𝐻 ) ) → 𝐴 = ( ( ( projℎ ‘ ( 𝐹 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
9 4 6 8 syl2an ⊢ ( ( ( 𝐴 ∈ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) ∧ 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) ) ∧ ( 𝐹 ⊆ ( ⊥ ‘ 𝐻 ) ∧ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) ) → 𝐴 = ( ( ( projℎ ‘ ( 𝐹 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
10 1 2 osumi ⊢ ( 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) → ( 𝐹 +ℋ 𝐺 ) = ( 𝐹 ∨ℋ 𝐺 ) )
11 10 fveq2d ⊢ ( 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) → ( projℎ ‘ ( 𝐹 +ℋ 𝐺 ) ) = ( projℎ ‘ ( 𝐹 ∨ℋ 𝐺 ) ) )
12 11 fveq1d ⊢ ( 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( projℎ ‘ ( 𝐹 +ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( projℎ ‘ ( 𝐹 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) )
13 12 oveq1d ⊢ ( 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( ( projℎ ‘ ( 𝐹 +ℋ 𝐺 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ ( 𝐹 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
14 13 ad2antlr ⊢ ( ( ( 𝐴 ∈ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) ∧ 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) ) ∧ ( 𝐹 ⊆ ( ⊥ ‘ 𝐻 ) ∧ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ ( 𝐹 +ℋ 𝐺 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( ( projℎ ‘ ( 𝐹 ∨ℋ 𝐺 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
15 7 3 chjcli ⊢ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) ∈ Cℋ
16 15 cheli ⊢ ( 𝐴 ∈ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) → 𝐴 ∈ ℋ )
17 1 2 pjsumi ⊢ ( 𝐴 ∈ ℋ → ( 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) → ( ( projℎ ‘ ( 𝐹 +ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ 𝐹 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ) )
18 17 imp ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) ) → ( ( projℎ ‘ ( 𝐹 +ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ 𝐹 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )
19 16 18 sylan ⊢ ( ( 𝐴 ∈ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) ∧ 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) ) → ( ( projℎ ‘ ( 𝐹 +ℋ 𝐺 ) ) ‘ 𝐴 ) = ( ( ( projℎ ‘ 𝐹 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) )
20 19 oveq1d ⊢ ( ( 𝐴 ∈ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) ∧ 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) ) → ( ( ( projℎ ‘ ( 𝐹 +ℋ 𝐺 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( ( ( projℎ ‘ 𝐹 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
21 20 adantr ⊢ ( ( ( 𝐴 ∈ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) ∧ 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) ) ∧ ( 𝐹 ⊆ ( ⊥ ‘ 𝐻 ) ∧ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ ( 𝐹 +ℋ 𝐺 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = ( ( ( ( projℎ ‘ 𝐹 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
22 9 14 21 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ( ( 𝐹 ∨ℋ 𝐺 ) ∨ℋ 𝐻 ) ∧ 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) ) ∧ ( 𝐹 ⊆ ( ⊥ ‘ 𝐻 ) ∧ 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) ) ) → 𝐴 = ( ( ( ( projℎ ‘ 𝐹 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )